let X, Y be set ; for f being Function st dom f c= [:X,Y:] holds
rng (~ f) = rng f
let f be Function; ( dom f c= [:X,Y:] implies rng (~ f) = rng f )
assume A1:
dom f c= [:X,Y:]
; rng (~ f) = rng f
thus
rng (~ f) c= rng f
by Th41; XBOOLE_0:def 10 rng f c= rng (~ f)
let y be object ; TARSKI:def 3 ( not y in rng f or y in rng (~ f) )
assume
y in rng f
; y in rng (~ f)
then consider x being object such that
A2:
x in dom f
and
A3:
y = f . x
by FUNCT_1:def 3;
consider x1, y1 being object such that
x1 in X
and
y1 in Y
and
A4:
x = [x1,y1]
by A1, A2, ZFMISC_1:84;
A5:
[y1,x1] in dom (~ f)
by A2, A4, Th42;
y =
f . (x1,y1)
by A3, A4
.=
(~ f) . (y1,x1)
by A2, A4, Def2
;
hence
y in rng (~ f)
by A5, FUNCT_1:def 3; verum