let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A
let A be Subset of (E ^omega); :: thesis: for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A
let n be Nat; :: thesis: A |^.. (n + 1) = (A |^.. n) ^^ A

now :: thesis: for x being object st x in A |^.. (n + 1) holds
x in (A |^.. n) ^^ A

let x be object ; :: thesis: ( x in A |^.. (n + 1) implies x in (A |^.. n) ^^ A )
assume x in A |^.. (n + 1) ; :: thesis: x in (A |^.. n) ^^ A
then consider k being Nat such that
A1: n + 1 <= k and
A2: x in A |^ k by Th2;
consider l being Nat such that
A3: l + 1 = k by A1, NAT_1:6;
x in (A |^ l) ^^ (A |^ 1) by A2, A3, FLANG_1:33;
then consider a, b being Element of E ^omega such that
A4: a in A |^ l and
A5: b in A |^ 1 and
A6: x = a ^ b by FLANG_1:def 1;
n <= l by A1, A3, XREAL_1:6;
then a in A |^.. n by A4, Th2;
then x in (A |^.. n) ^^ (A |^ 1) by A5, A6, FLANG_1:def 1;
hence x in (A |^.. n) ^^ A by FLANG_1:25; :: thesis: verum

end;

then A7: A |^.. (n + 1) c= (A |^.. n) ^^ A ;

now :: thesis: for x being object st x in (A |^.. n) ^^ A holds
x in A |^.. (n + 1)

let x be object ; :: thesis: ( x in (A |^.. n) ^^ A implies x in A |^.. (n + 1) )
assume x in (A |^.. n) ^^ A ; :: thesis: x in A |^.. (n + 1)
then consider a, b being Element of E ^omega such that
A8: a in A |^.. n and
A9: b in A and
A10: x = a ^ b by FLANG_1:def 1;
consider k being Nat such that
A11: n <= k and
A12: a in A |^ k by A8, Th2;
A13: n + 1 <= k + 1 by A11, XREAL_1:6;
b in A |^ 1 by A9, FLANG_1:25;
then x in A |^ (k + 1) by A10, A12, FLANG_1:40;
hence x in A |^.. (n + 1) by A13, Th2; :: thesis: verum

end;

then (A |^.. n) ^^ A c= A |^.. (n + 1) ;
hence A |^.. (n + 1) = (A |^.. n) ^^ A by A7, XBOOLE_0:def 10; :: thesis: verum