let D be set ; for f being FinSequence of D st len f >= 2 holds
f | 2 = <*(f /. 1),(f /. 2)*>
let f be FinSequence of D; ( len f >= 2 implies f | 2 = <*(f /. 1),(f /. 2)*> )
set d1 = f /. 1;
set d2 = f /. 2;
assume A1:
len f >= 2
; f | 2 = <*(f /. 1),(f /. 2)*>
then A2:
len (f | 2) = 2
by FINSEQ_1:59;
reconsider D = D as non empty set by A1;
reconsider f = f as FinSequence of D ;
2 in dom (f | 2)
by A2, FINSEQ_3:25;
then A3: f /. 2 =
(f | 2) /. 2
by FINSEQ_4:70
.=
(f | 2) . 2
by A2, FINSEQ_4:15
;
1 in dom (f | 2)
by A2, FINSEQ_3:25;
then f /. 1 =
(f | 2) /. 1
by FINSEQ_4:70
.=
(f | 2) . 1
by A2, FINSEQ_4:15
;
hence
f | 2 = <*(f /. 1),(f /. 2)*>
by A2, A3, FINSEQ_1:44; verum