let f be FinSequence of (TOP-REAL 2); :: thesis: X_axis f = proj1 * f
reconsider pf = proj1 * f as FinSequence of REAL by FINSEQ_2:32;
A1: len (X_axis f) = len f by GOBOARD1:def 1;
then A2: dom (X_axis f) = dom f by FINSEQ_3:29;
A3: for k being Nat st k in dom (X_axis f) holds
(X_axis f) . k = pf . k

proof

let k be Nat; :: thesis: ( k in dom (X_axis f) implies (X_axis f) . k = pf . k )
assume A4: k in dom (X_axis f) ; :: thesis: (X_axis f) . k = pf . k
A5: f /. k = f . k by A2, A4, PARTFUN1:def 6;
thus (X_axis f) . k = (f /. k) `1 by A4, GOBOARD1:def 1
.= proj1 . (f . k) by A5, PSCOMP_1:def 5
.= pf . k by A2, A4, FUNCT_1:13 ; :: thesis: verum

end;

len pf = len f by FINSEQ_2:33;
then dom (X_axis f) = dom pf by A1, FINSEQ_3:29;
hence X_axis f = proj1 * f by A3, FINSEQ_1:13; :: thesis: verum