let A be Universal_Algebra; :: thesis: for B being Subset of A
for n, m being Nat st n <= m holds
B |^ n c= B |^ m
let B be Subset of A; :: thesis: for n, m being Nat st n <= m holds
B |^ n c= B |^ m
let n, m be Nat; :: thesis: ( n <= m implies B |^ n c= B |^ m )
assume n <= m ; :: thesis: B |^ n c= B |^ m
then A1: ex i being Nat st m = n + i by NAT_1:10;
defpred S1[ Nat] means B |^ n c= B |^ (n + $1);
A2: S1[ 0 ] ;
A3: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; :: thesis: S1[i + 1]
deffunc H1( set , set ) -> set = $2 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= $2 ) } ;
B |^ ((n + i) + 1) = H1(n,B |^ (n + i)) by Th19;
then B |^ (n + i) c= B |^ (n + (i + 1)) by XBOOLE_1:7;
hence S1[i + 1] by A4, XBOOLE_1:1; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A2, A3);
 hence B |^ n c= B |^ m by A1; :: thesis: verum