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)*>
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 A1: len (IDEA_P_F Key,n,(k + 1)) = len ((IDEA_P_F Key,n,k) ^ <*(IDEA_P (Line Key,(k + 1)),n)*>) by Def17;
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

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 A2: ( 1 <= i & 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
then A3: ( 1 <= i & i <= k + 1 ) by Def17;
i in Seg (len (IDEA_P_F Key,n,(k + 1))) by A2, FINSEQ_1:3;
then A4: i in dom (IDEA_P_F Key,n,(k + 1)) by FINSEQ_1:def 3;
dom <*(IDEA_P (Line Key,(k + 1)),n)*> = Seg 1 by FINSEQ_1:def 8;
then A5: 1 in dom <*(IDEA_P (Line Key,(k + 1)),n)*> by FINSEQ_1:3;

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 ( 1 <= i & i <= k ) by A3, NAT_1:8;
then i in Seg k by FINSEQ_1:3;
then i in Seg (len (IDEA_P_F Key,n,k)) by Def17;
then A6: 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 A6, Def17
.= (IDEA_P_F Key,n,(k + 1)) . i by A4, Def17 ;
:: thesis: verum

end;

suppose A7: 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 A5, FINSEQ_1:def 7
.= IDEA_P (Line Key,(k + 1)),n by FINSEQ_1:57
.= (IDEA_P_F Key,n,(k + 1)) . i by A4, A7, 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;

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