let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( rng f c= rng g implies rng (Y_axis f) c= rng (Y_axis g) )
assume A1: rng f c= rng g ; :: thesis: rng (Y_axis f) c= rng (Y_axis g)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Y_axis f) or x in rng (Y_axis g) )
assume x in rng (Y_axis f) ; :: thesis: x in rng (Y_axis g)
then consider y being set such that
A2: y in dom (Y_axis f) and
A3: (Y_axis f) . y = x by FUNCT_1:def 5;
A4: dom (Y_axis f) = dom f by SPRECT_2:20;
A5: dom (Y_axis g) = dom g by SPRECT_2:20;
reconsider y = y as Element of NAT by A2;
A6: (Y_axis f) . y = (f /. y) `2 by A2, GOBOARD1:def 4;
f /. y in rng f by A2, A4, PARTFUN2:4;
then consider z being set such that
A7: z in dom g and
A8: g . z = f /. y by A1, FUNCT_1:def 5;
reconsider z = z as Element of NAT by A7;
g /. z = f /. y by A7, A8, PARTFUN1:def 8;
then (Y_axis g) . z = (f /. y) `2 by A5, A7, GOBOARD1:def 4;
hence x in rng (Y_axis g) by A3, A5, A6, A7, FUNCT_1:def 5; :: thesis: verum