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

per cases ( m <= n or m > n ) ;

suppose m <= n ; :: thesis: A |^ (m + 1),(n + 1) = (A |^ m,n) ^^ A

hence A |^ (m + 1),(n + 1) = (A |^ m,n) ^^ (A |^ 1,1) by Th37
.= (A |^ m,n) ^^ (A |^ 1) by Th22
.= (A |^ m,n) ^^ A by FLANG_1:26 ;
:: thesis: verum

end;

suppose A1: m > n ; :: thesis: A |^ (m + 1),(n + 1) = (A |^ m,n) ^^ A

then A |^ m,n = {} by Th21;
then A2: (A |^ m,n) ^^ A = {} by FLANG_1:13;
m + 1 > n + 1 by A1, XREAL_1:10;
hence A |^ (m + 1),(n + 1) = (A |^ m,n) ^^ A by A2, Th21; :: thesis: verum

end;

end;