set P = E -class ;
now :: thesis: for c being object st c in Class E holds
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;
then ( Class E c= rng (E -class) & rng (E -class) c= Class E ) by RELAT_1:def 19, TARSKI:def 3;
hence for b1 being Function of X,(Class E) st b1 = E -class holds
b1 is onto by FUNCT_2:def 3, XBOOLE_0:def 10; :: thesis: verum