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:32;
A1: len (Y_axis f) = len f by GOBOARD1:def 2;
then A2: dom (Y_axis f) = dom f by FINSEQ_3:29;
A3: 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 A4: k in dom (Y_axis f) ; :: thesis: (Y_axis f) . k = pf . k
A5: f /. k = f . k by A2, A4, PARTFUN1:def 6;
thus (Y_axis f) . k = (f /. k) `2 by A4, GOBOARD1:def 2
.= proj2 . (f . k) by A5, PSCOMP_1:def 6
.= pf . k by A2, A4, FUNCT_1:13 ; :: thesis: verum
end;
len pf = len f by FINSEQ_2:33;
then dom (Y_axis f) = dom pf by A1, FINSEQ_3:29;
hence Y_axis f = proj2 * f by A3, FINSEQ_1:13; :: thesis: verum