let X, Y be set ; :: thesis: for f being Function st dom f c= [:X,Y:] holds
rng (~ f) = rng f
let f be Function; :: thesis: ( dom f c= [:X,Y:] implies rng (~ f) = rng f )
assume A1: dom f c= [:X,Y:] ; :: thesis: rng (~ f) = rng f
thus rng (~ f) c= rng f by Th41; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (~ f)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in rng (~ f) )
assume y in rng f ; :: thesis: 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; :: thesis: verum