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:25 ;
:: 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:12;
m + 1 > n + 1 by A1, XREAL_1:8;
hence A |^ ((m + 1),(n + 1)) = (A |^ (m,n)) ^^ A by A2, Th21; :: thesis: verum
end;
end;