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_Q_F Key,n,(k + 1) = <*(IDEA_Q (Line Key,(k + 1)),n)*> ^ (IDEA_Q_F Key,n,k)
let lk be Element of NAT ; :: thesis: for Key being Matrix of lk,6, NAT
for k being Element of 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 Element of 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 Element of 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:3;
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:3;
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:3;
then A7: i in dom (IDEA_Q_F Key,n,(k + 1)) by FINSEQ_1:def 3;

now

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:11;
1 - 1 <= i - 1 by A3, XREAL_1:11;
then reconsider ii = ii as Element of NAT by A9, INT_1:16;
A12: i - 1 <= (k + 1) - 1 by A5, XREAL_1:11;
then ii - ii <= k - ii by A9, XREAL_1:11;
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:11;
then ii in Seg k by A9, A12, FINSEQ_1:3;
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:57
.= (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 by FINSEQ_1:57
.= IDEA_Q (Line Key,(((k + 1) -' 1) + 1)),n by A3, A5, XREAL_1:237, 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:35
.= (len <*(IDEA_Q (Line Key,(k + 1)),n)*>) + k by Def18
.= k + 1 by FINSEQ_1:56 ;
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:18; :: thesis: verum