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

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

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

then A7:
A |^.. (n + 1) c= (A |^.. n) ^^ A
;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;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

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

x in A |^.. (n + 1)

then
(A |^.. n) ^^ A c= A |^.. (n + 1)
;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;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

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