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

let A be Subset of (); :: 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 ;
x in (A |^ l) ^^ (A |^ 1) by ;
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 ;
then a in A |^.. n by ;
then x in (A |^.. n) ^^ (A |^ 1) by ;
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 ;
A13: n + 1 <= k + 1 by ;
b in A |^ 1 by ;
then x in A |^ (k + 1) by ;
hence x in A |^.. (n + 1) by ; :: thesis: verum
end;
then (A |^.. n) ^^ A c= A |^.. (n + 1) ;
hence A |^.. (n + 1) = (A |^.. n) ^^ A by ; :: thesis: verum