let n be non zero Nat; :: thesis: for lk being Nat
for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_P_F (Key,n,(k + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>
let lk be Nat; :: thesis: for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_P_F (Key,n,(k + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>
let Key be Matrix of lk,6,NAT; :: thesis: for k being Nat holds IDEA_P_F (Key,n,(k + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>
let k be Nat; :: thesis: IDEA_P_F (Key,n,(k + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>
A1: for i being Nat st 1 <= i & i <= len (IDEA_P_F (Key,n,(k + 1))) holds
(IDEA_P_F (Key,n,(k + 1))) . i = ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i

proof

dom <*(IDEA_P ((Line (Key,(k + 1))),n))*> = Seg 1 by FINSEQ_1:def 8;
then A2: 1 in dom <*(IDEA_P ((Line (Key,(k + 1))),n))*> by FINSEQ_1:1;
let i be Nat; :: thesis: ( 1 <= i & i <= len (IDEA_P_F (Key,n,(k + 1))) implies (IDEA_P_F (Key,n,(k + 1))) . i = ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i )
assume that
A3: 1 <= i and
A4: i <= len (IDEA_P_F (Key,n,(k + 1))) ; :: thesis: (IDEA_P_F (Key,n,(k + 1))) . i = ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i
i in Seg (len (IDEA_P_F (Key,n,(k + 1)))) by A3, A4, FINSEQ_1:1;
then A5: i in dom (IDEA_P_F (Key,n,(k + 1))) by FINSEQ_1:def 3;
A6: i <= k + 1 by A4, Def17;

now :: thesis: ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i = (IDEA_P_F (Key,n,(k + 1))) . i

per cases ( i <> k + 1 or i = k + 1 ) ;

suppose i <> k + 1 ; :: thesis: ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i = (IDEA_P_F (Key,n,(k + 1))) . i

then i <= k by A6, NAT_1:8;
then i in Seg k by A3, FINSEQ_1:1;
then i in Seg (len (IDEA_P_F (Key,n,k))) by Def17;
then A7: i in dom (IDEA_P_F (Key,n,k)) by FINSEQ_1:def 3;
hence ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i = (IDEA_P_F (Key,n,k)) . i by FINSEQ_1:def 7
.= IDEA_P ((Line (Key,i)),n) by A7, Def17
.= (IDEA_P_F (Key,n,(k + 1))) . i by A5, Def17 ;
:: thesis: verum

end;

suppose A8: i = k + 1 ; :: thesis: ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i = (IDEA_P_F (Key,n,(k + 1))) . i

hence ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i = ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . ((len (IDEA_P_F (Key,n,k))) + 1) by Def17
.= <*(IDEA_P ((Line (Key,(k + 1))),n))*> . 1 by A2, FINSEQ_1:def 7
.= IDEA_P ((Line (Key,(k + 1))),n)
.= (IDEA_P_F (Key,n,(k + 1))) . i by A5, A8, Def17 ;
:: thesis: verum

end;

end;

end;

hence (IDEA_P_F (Key,n,(k + 1))) . i = ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) . i ; :: thesis: verum

end;

len ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) = (len (IDEA_P_F (Key,n,k))) + (len <*(IDEA_P ((Line (Key,(k + 1))),n))*>) by FINSEQ_1:22
.= k + (len <*(IDEA_P ((Line (Key,(k + 1))),n))*>) by Def17
.= k + 1 by FINSEQ_1:39 ;
then len (IDEA_P_F (Key,n,(k + 1))) = len ((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>) by Def17;
hence IDEA_P_F (Key,n,(k + 1)) = (IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*> by A1, FINSEQ_1:14; :: thesis: verum