let f be Function; :: 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
A1: x in dom (~ f) and
A2: y = (~ f) . x by FUNCT_1:def 3;
consider x1, x2 being object such that
A3: x = [x2,x1] and
A4: [x1,x2] in dom f by A1, Def2;
y = (~ f) . (x2,x1) by A2, A3
.= f . (x1,x2) by A4, Def2 ;
hence y in rng f by A4, FUNCT_1:def 3; :: thesis: verum