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 S1[ Nat] means A * = (A *) ^^ (A |^ (m,(m + $1)));
A4: 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 A5: S1[i] ; :: thesis: S1[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 S1[i + 1] ; :: thesis: verum
end;
A * = (A *) ^^ (A |^ m) by A1, FLANG_1:55
.= (A *) ^^ (A |^ (m,(m + 0))) by Th22 ;
then A6: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A6, A4);
 hence A * = (A *) ^^ (A |^ (m,n)) by A3; :: thesis: verum