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

proof

let m, n be Nat; :: thesis: ( m + n <= 0 implies A |^ (m + n) = (A |^ m) ^^ (A |^ n) )
assume m + n <= 0 ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
then A2: m + n = 0 ;
then A3: ( m = 0 & n = 0 ) ;
thus A |^ (m + n) = (A |^ 0 ) ^^ {(<%> E)} by A2, Th14
.= (A |^ m) ^^ (A |^ n) by A3, Th25 ; :: thesis: verum

end;

A4: now

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A5: S₁[l] ; :: thesis: S₁[l + 1]

now

let m, n be Nat; :: thesis: ( m + n <= l + 1 implies A |^ (m + n) = (A |^ m) ^^ (A |^ n) )
assume A6: m + n <= l + 1 ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)

A7: now

assume A8: m + n = l + 1 ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)

A9: now

assume A10: m = 0 ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
thus A |^ (m + n) = {(<%> E)} ^^ (A |^ (l + 1)) by A8, Th14
.= (A |^ m) ^^ (A |^ n) by A8, A10, Th25 ; :: thesis: verum

end;

A11: now

assume A12: n = 0 ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
thus A |^ (m + n) = (A |^ (l + 1)) ^^ {(<%> E)} by A8, Th14
.= (A |^ m) ^^ (A |^ n) by A8, A12, Th25 ; :: thesis: verum

end;

now

assume A13: ( m > 0 & n > 0 ) ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
then consider k being Nat such that
A14: k + 1 = m by NAT_1:6;
A |^ (m + n) = A |^ ((k + n) + 1) by A14
.= (A |^ (k + n)) ^^ A by Th24
.= A ^^ (A |^ (k + n)) by Th33
.= A ^^ ((A |^ k) ^^ (A |^ n)) by A5, A8, A14
.= (A ^^ (A |^ k)) ^^ (A |^ n) by Th19
.= ((A |^ k) ^^ A) ^^ (A |^ n) by Th33
.= ((A |^ k) ^^ (A |^ 1)) ^^ (A |^ n) by Th26
.= (A |^ m) ^^ (A |^ n) by A5, A8, A13, A14, Th2 ;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) ; :: thesis: verum

end;

hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A9, A11; :: thesis: verum

end;

now

assume m + n < l + 1 ; :: thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
then m + n <= l by NAT_1:13;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A5; :: thesis: verum

end;

hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A6, A7, XXREAL_0:1; :: thesis: verum

end;

hence S₁[l + 1] ; :: thesis: verum

end;

for l being Nat holds S₁[l] from NAT_1:sch 2(A1, A4);
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) ; :: thesis: verum