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 by FUNCT_2:def 3;
let xx be set ; :: 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, x' being set such that
A3: xx = [x,x'] by RELAT_1:def 1;
A4: x = x' by A2, A3, RELAT_1:def 10;
A5: x in B by A2, A3, RELAT_1:def 10;
then consider y being set such that
A6: y in A and
A7: f . y = x by A1, FUNCT_2:17;
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 9;
hence xx in [:f,f:] .: (id A) by A2, A9, FUNCT_2:43; :: thesis: verum