let E be set ; :: thesis: for A being Subset of (E ^omega )
for k being Nat holds (A ? ) |^ k = A |^ 0 ,k
let A be Subset of (E ^omega ); :: thesis: for k being Nat holds (A ? ) |^ k = A |^ 0 ,k
let k be Nat; :: thesis: (A ? ) |^ k = A |^ 0 ,k
defpred S₁[ Nat] means (A ? ) |^ $1 = A |^ 0 ,$1;
A1: S₁[ 0 ]

proof

thus (A ? ) |^ 0 = {(<%> E)} by FLANG_1:25
.= A |^ 0 ,0 by Th45 ; :: thesis: verum

end;

A2: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
(A ? ) |^ (k + 1) = ((A ? ) |^ k) ^^ ((A ? ) |^ 1) by FLANG_1:34
.= (A |^ 0 ,k) ^^ (A ? ) by A3, FLANG_1:26
.= (A |^ 0 ,k) ^^ (A |^ 0 ,1) by Th79
.= A |^ (0 + 0 ),(k + 1) by Th37 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (A ? ) |^ k = A |^ 0 ,k ; :: thesis: verum