let i be Nat; :: thesis: for f being FinSequence of (TOP-REAL 2) st i in dom f holds
( (X_axis f) . i = (f /. i) `1 & (Y_axis f) . i = (f /. i) `2 )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( i in dom f implies ( (X_axis f) . i = (f /. i) `1 & (Y_axis f) . i = (f /. i) `2 ) )
assume A1: i in dom f ; :: thesis: ( (X_axis f) . i = (f /. i) `1 & (Y_axis f) . i = (f /. i) `2 )
len (X_axis f) = len f by GOBOARD1:def 1;
then i in dom (X_axis f) by A1, FINSEQ_3:29;
hence (X_axis f) . i = (f /. i) `1 by GOBOARD1:def 1; :: thesis: (Y_axis f) . i = (f /. i) `2
len (Y_axis f) = len f by GOBOARD1:def 2;
then i in dom (Y_axis f) by A1, FINSEQ_3:29;
hence (Y_axis f) . i = (f /. i) `2 by GOBOARD1:def 2; :: thesis: verum