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 Th42; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (~ f)
let y be set ; :: 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 set such that
A2: x in dom f and
A3: y = f . x by FUNCT_1:def 5;
consider x1, y1 being set such that
( x1 in X & y1 in Y ) and
A4: x = [x1,y1] by A1, A2, ZFMISC_1:103;
A5: [y1,x1] in dom (~ f) by A2, A4, Th43;
y = f . x1,y1 by A3, A4
.= (~ f) . y1,x1 by A2, A4, Def2 ;
hence y in rng (~ f) by A5, FUNCT_1:def 5; :: thesis: verum