let n be non zero Nat; 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; 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; 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; 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;
( 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)))
;
(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 (<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . i = (IDEA_Q_F (Key,n,(k + 1))) . iper cases
( i <> 1 or i = 1 )
;
suppose A8:
i <> 1
;
(<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . i = (IDEA_Q_F (Key,n,(k + 1))) . iconsider 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
;
verum end; suppose A15:
i = 1
;
(<*(IDEA_Q ((Line (Key,(k + 1))),n))*> ^ (IDEA_Q_F (Key,n,k))) . i = (IDEA_Q_F (Key,n,(k + 1))) . ihence (<*(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:40
.=
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
;
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
;
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; verum