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