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