let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat st <%> E in A & m <= n holds
A * = (A * ) ^^ (A |^ m,n)
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat st <%> E in A & m <= n holds
A * = (A * ) ^^ (A |^ m,n)
let m, n be Nat; :: thesis: ( <%> E in A & m <= n implies A * = (A * ) ^^ (A |^ m,n) )
assume that
A1: <%> E in A and
A2: m <= n ; :: thesis: A * = (A * ) ^^ (A |^ m,n)
A3: ex k being Nat st m + k = n by A2, NAT_1:10;
defpred S₁[ Nat] means A * = (A * ) ^^ (A |^ m,(m + $1));

A4: now

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
A |^ m,(m + (i + 1)) = (A |^ m,(m + i)) \/ (A |^ ((m + i) + 1)) by Th26, NAT_1:11;
then (A * ) ^^ (A |^ m,(m + (i + 1))) = (A * ) \/ ((A * ) ^^ (A |^ ((m + i) + 1))) by A5, FLANG_1:21
.= (A * ) \/ (A * ) by A1, FLANG_1:56 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A * = (A * ) ^^ (A |^ m) by A1, FLANG_1:56
.= (A * ) ^^ (A |^ m,(m + 0 )) by Th22 ;
then A6: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A4);
hence A * = (A * ) ^^ (A |^ m,n) by A3; :: thesis: verum