let A, B be set ; :: thesis: for f being Function of A,B st f is onto holds
id B c= [:f,f:] .: (id A)
let f be Function of A,B; :: thesis: ( f is onto implies id B c= [:f,f:] .: (id A) )
assume f is onto ; :: thesis: id B c= [:f,f:] .: (id A)
then A1: rng f = B ;
let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in id B or xx in [:f,f:] .: (id A) )
assume A2: xx in id B ; :: thesis: xx in [:f,f:] .: (id A)
then consider x, x9 being object such that
A3: xx = [x,x9] by RELAT_1:def 1;
A4: x = x9 by A2, A3, RELAT_1:def 10;
A5: x in B by A2, A3, RELAT_1:def 10;
then consider y being object such that
A6: y in A and
A7: f . y = x by A1, FUNCT_2:11;
A8: dom f = A by A5, FUNCT_2:def 1;
A9: [y,y] in id A by A6, RELAT_1:def 10;
[:f,f:] . (y,y) = xx by A3, A4, A6, A7, A8, FUNCT_3:def 8;
hence xx in [:f,f:] .: (id A) by A2, A9, FUNCT_2:35; :: thesis: verum