let n, k be Nat; 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)*>)
;
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;
( 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)))
;
(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
hence
(NPower (n,(k + 1))) . l = ((NPower (n,k)) ^ <*((k + 1) |^ n)*>) . l
by Def8, A4;
verum
end;
hence
NPower (n,(k + 1)) = (NPower (n,k)) ^ <*((k + 1) |^ n)*>
by A1, FINSEQ_1:13; verum