let n, k be Nat; :: thesis: NPower (n,(k + 1)) = (NPower (n,k)) ^ <*((k + 1) |^ n)*>
A1: dom (NPower (n,(k + 1))) = dom ((NPower (n,k)) ^ <*((k + 1) |^ n)*>)
proof
Seg (len (NPower (n,k))) = dom (NPower (n,k)) by FINSEQ_1:def 3
.= Seg k by Def8 ;
then A2: len (NPower (n,k)) = k by FINSEQ_1:6;
A3: len <*((k + 1) |^ n)*> = 1 by FINSEQ_1:40;
dom ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) = Seg ((len (NPower (n,k))) + (len <*((k + 1) |^ n)*>)) by FINSEQ_1:def 7
.= dom (NPower (n,(k + 1))) by Def8, A3, A2 ;
hence dom (NPower (n,(k + 1))) = dom ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) ; :: thesis: verum
end;
for l being Nat st l in dom (NPower (n,(k + 1))) holds
(NPower (n,(k + 1))) . l = ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l
proof
let l be Nat; :: thesis: ( l in dom (NPower (n,(k + 1))) implies (NPower (n,(k + 1))) . l = ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l )
assume A4: l in dom (NPower (n,(k + 1))) ; :: thesis: (NPower (n,(k + 1))) . l = ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l
then l in Seg (k + 1) by Def8;
then A5: ( 1 <= l & l <= k + 1 ) by FINSEQ_1:1;
set NP = ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l;
((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l = l |^ n
proof
per cases ( l <= k or l = k + 1 ) by A5, NAT_1:8;
suppose l <= k ; :: thesis: ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l = l |^ n
then l in Seg k by A5, FINSEQ_1:1;
then A6: l in dom (NPower (n,k)) by Def8;
then ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l = (NPower (n,k)) . l by FINSEQ_1:def 7
.= l |^ n by Def8, A6 ;
hence ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l = l |^ n ; :: thesis: verum
end;
suppose A7: l = k + 1 ; :: thesis: ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l = l |^ n
Seg k = dom (NPower (n,k)) by Def8
.= Seg (len (NPower (n,k))) by FINSEQ_1:def 3 ;
then k = len (NPower (n,k)) by FINSEQ_1:6;
hence ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l = l |^ n by A7, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
hence (NPower (n,(k + 1))) . l = ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l by Def8, A4; :: thesis: verum
end;
hence NPower (n,(k + 1)) = (NPower (n,k)) ^ <*((k + 1) |^ n)*> by A1, FINSEQ_1:13; :: thesis: verum