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 A1: ( <%> E in A & m <= n ) ; :: thesis: A * = (A * ) ^^ (A |^ m,n)
defpred S₁[ Nat] means A * = (A * ) ^^ (A |^ m,(m + $1));
A2: S₁[ 0 ]

proof

thus A * = (A * ) ^^ (A |^ m) by A1, FLANG_1:56
.= (A * ) ^^ (A |^ m,(m + 0 )) by Th22 ; :: thesis: verum

end;

A3: now

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: 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 A4, FLANG_1:21
.= (A * ) \/ (A * ) by A1, FLANG_1:56 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A5: for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
consider k being Nat such that
A6: m + k = n by A1, NAT_1:10;
thus A * = (A * ) ^^ (A |^ m,n) by A5, A6; :: thesis: verum