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 :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

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:20
.= (A *) \/ (A *) by A1, FLANG_1:55 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A * = (A *) ^^ (A |^ m) by A1, FLANG_1:55
.= (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