let f be FinSequence of (TOP-REAL 2); :: thesis: Y_axis f = proj2 * f
reconsider pf = proj2 * f as FinSequence of REAL by FINSEQ_2:36;
A1: len pf = len f by FINSEQ_2:37;
A2: len (Y_axis f) = len f by GOBOARD1:def 4;
then A3: dom (Y_axis f) = dom f by FINSEQ_3:31;
A4: dom (Y_axis f) = dom pf by A1, A2, FINSEQ_3:31;
for k being Nat st k in dom (Y_axis f) holds
(Y_axis f) . k = pf . k

proof

let k be Nat; :: thesis: ( k in dom (Y_axis f) implies (Y_axis f) . k = pf . k )
assume A5: k in dom (Y_axis f) ; :: thesis: (Y_axis f) . k = pf . k
A6: f /. k = f . k by A3, A5, PARTFUN1:def 8;
thus (Y_axis f) . k = (f /. k) `2 by A5, GOBOARD1:def 4
.= proj2 . (f . k) by A6, PSCOMP_1:def 29
.= pf . k by A3, A5, FUNCT_1:23 ; :: thesis: verum

end;

hence Y_axis f = proj2 * f by A4, FINSEQ_1:17; :: thesis: verum