let D be set ; :: thesis: for f being FinSequence of D st len f >= 2 holds
f | 2 = <*(f /. 1),(f /. 2)*>
let f be FinSequence of D; :: thesis: ( len f >= 2 implies f | 2 = <*(f /. 1),(f /. 2)*> )
set d1 = f /. 1;
set d2 = f /. 2;
assume A1: len f >= 2 ; :: thesis: f | 2 = <*(f /. 1),(f /. 2)*>
then A2: len (f | 2) = 2 by FINSEQ_1:80;

now

assume A3: D is empty ; :: thesis: contradiction
rng f c= D by FINSEQ_1:def 4;
then f = {} by A3;
hence contradiction by A1; :: thesis: verum

end;

then reconsider D = D as non empty set ;
reconsider f = f as FinSequence of D ;
2 in dom (f | 2) by A2, FINSEQ_3:27;
then A4: f /. 2 = (f | 2) /. 2 by FINSEQ_4:85
.= (f | 2) . 2 by A2, FINSEQ_4:24 ;
1 in dom (f | 2) by A2, FINSEQ_3:27;
then f /. 1 = (f | 2) /. 1 by FINSEQ_4:85
.= (f | 2) . 1 by A2, FINSEQ_4:24 ;
hence f | 2 = <*(f /. 1),(f /. 2)*> by A2, A4, FINSEQ_1:61; :: thesis: verum