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_Q_F (Key,n,(k + 1)) = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))
let lk be Nat; :: thesis: for Key being Matrix of lk,6,NAT
for k being Nat holds IDEA_Q_F (Key,n,(k + 1)) = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))
let Key be Matrix of lk,6,NAT; :: thesis: for k being Nat holds IDEA_Q_F (Key,n,(k + 1)) = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))
let k be Nat; :: thesis: IDEA_Q_F (Key,n,(k + 1)) = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))
A1: for i being Nat st 1 <= i & i <= len (IDEA_Q_F (Key,n,(k + 1))) holds
(IDEA_Q_F (Key,n,(k + 1))) . i = (<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . i

proof

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

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

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

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

consider ii being Integer such that
A9: ii = i - 1 ;
A10: ii + 1 = i by A9;
A11: (k + 1) - i >= i - i by A5, XREAL_1:9;
1 - 1 <= i - 1 by A3, XREAL_1:9;
then reconsider ii = ii as Element of NAT by A9, INT_1:3;
A12: i - 1 <= (k + 1) - 1 by A5, XREAL_1:9;
then ii - ii <= k - ii by A9, XREAL_1:9;
then A13: k -' ii = (k + 1) + (- i) by A9, XREAL_0:def 2
.= (k + 1) -' i by A11, XREAL_0:def 2 ;
1 < i by A3, A8, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then (1 + 1) - 1 <= i - 1 by XREAL_1:9;
then ii in Seg k by A9, A12, FINSEQ_1:1;
then ii in Seg (len (IDEA_Q_F (Key,n,k))) by Def18;
then A14: ii in dom (IDEA_Q_F (Key,n,k)) by FINSEQ_1:def 3;
thus (<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . i = (<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . ((len <*(IDEA_Q ((Line (Key,(k + 1))),n))*>) + ii) by A10, FINSEQ_1:40
.= (IDEA_Q_F (Key,n,k)) . ii by A14, FINSEQ_1:def 7
.= IDEA_Q ((Line (Key,(((k + 1) -' i) + 1))),n) by A14, A13, Def18
.= (IDEA_Q_F (Key,n,(k + 1))) . i by A7, Def18 ; :: thesis: verum

end;

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

hence (<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . i = <*(IDEA_Q ((Line (Key,(k + 1))),n))*> . 1 by A2, FINSEQ_1:def 7
.= IDEA_Q ((Line (Key,(k + 1))),n)
.= IDEA_Q ((Line (Key,(((k + 1) -' 1) + 1))),n) by A3, A5, XREAL_1:235, XXREAL_0:2
.= (IDEA_Q_F (Key,n,(k + 1))) . i by A6, A15, Def18 ;
:: thesis: verum

end;

end;

end;

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

end;

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