let P be FinSequence-membered set ; :: thesis: for m, n being Nat holds P ^^ (m + n) = (P ^^ m) ^ (P ^^ n)
let m be Nat; :: thesis: for n being Nat holds P ^^ (m + n) = (P ^^ m) ^ (P ^^ n)
defpred S₁[ Nat] means P ^^ (m + $1) = (P ^^ m) ^ (P ^^ $1);
A1: S₁[ 0 ]

proof

thus P ^^ (m + 0) = (P ^^ m) ^ {{}} by Th3
.= (P ^^ m) ^ (P ^^ 0) by Th6 ; :: thesis: verum

end;

A20: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A21: P ^^ (m + k) = (P ^^ m) ^ (P ^^ k) ; :: thesis: S₁[k + 1]
thus P ^^ (m + (k + 1)) = P ^^ ((m + k) + 1)
.= ((P ^^ m) ^ (P ^^ k)) ^ P by Th6, A21
.= (P ^^ m) ^ ((P ^^ k) ^ P) by Th2
.= (P ^^ m) ^ (P ^^ (k + 1)) by Th6 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A20);
hence for n being Nat holds P ^^ (m + n) = (P ^^ m) ^ (P ^^ n) ; :: thesis: verum