let n be non empty Element of NAT ; :: thesis: for lk being Element of NAT
for Key being Matrix of lk,6, NAT
for k being Element of 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 Element of NAT ; :: thesis: for Key being Matrix of lk,6, NAT
for k being Element of 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 Element of 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 Element of 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:3;
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:3;
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

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:3;
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 by FINSEQ_1:57
.= (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:35
.= k + (len <*(IDEA_P (Line Key,(k + 1)),n)*>) by Def17
.= k + 1 by FINSEQ_1:56 ;
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:18; :: thesis: verum