set P = E -class ;

hence for b_{1} being Function of X,(Class E) st b_{1} = E -class holds

b_{1} is onto
by FUNCT_2:def 3, XBOOLE_0:def 10; :: thesis: verum

now :: thesis: for c being object st c in Class E holds

c in rng (E -class)

then
( Class E c= rng (E -class) & rng (E -class) c= Class E )
by RELAT_1:def 19, TARSKI:def 3;c in rng (E -class)

let c be object ; :: thesis: ( c in Class E implies c in rng (E -class) )

assume A1: c in Class E ; :: thesis: c in rng (E -class)

then reconsider cc = c as Subset of X ;

consider x being object such that

A2: ( x in X & cc = Class (E,x) ) by EQREL_1:def 3, A1;

reconsider xx = x as Element of X by A2;

(E -class) . xx = cc by A2, Def13;

hence c in rng (E -class) by FUNCT_2:4; :: thesis: verum

end;assume A1: c in Class E ; :: thesis: c in rng (E -class)

then reconsider cc = c as Subset of X ;

consider x being object such that

A2: ( x in X & cc = Class (E,x) ) by EQREL_1:def 3, A1;

reconsider xx = x as Element of X by A2;

(E -class) . xx = cc by A2, Def13;

hence c in rng (E -class) by FUNCT_2:4; :: thesis: verum

hence for b

b