let A be set ; :: thesis: for f being Function holds f .: (id A) = (~ f) .: (id A)
let f be Function; :: thesis: f .: (id A) = (~ f) .: (id A)
thus f .: (id A) c= (~ f) .: (id A) :: according to XBOOLE_0:def 10 :: thesis: (~ f) .: (id A) c= f .: (id A)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (id A) or y in (~ f) .: (id A) )
assume y in f .: (id A) ; :: thesis: y in (~ f) .: (id A)
then consider x being object such that
A1: x in dom f and
A2: x in id A and
A3: y = f . x by FUNCT_1:def 6;
consider x1, x2 being object such that
A4: x = [x1,x2] by A2, RELAT_1:def 1;
A5: x1 = x2 by A2, A4, RELAT_1:def 10;
then A6: x in dom (~ f) by A1, A4, FUNCT_4:42;
then f . (x1,x2) = (~ f) . (x1,x2) by A4, A5, FUNCT_4:43;
hence y in (~ f) .: (id A) by A2, A3, A4, A6, FUNCT_1:def 6; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (~ f) .: (id A) or y in f .: (id A) )
assume y in (~ f) .: (id A) ; :: thesis: y in f .: (id A)
then consider x being object such that
A7: x in dom (~ f) and
A8: x in id A and
A9: y = (~ f) . x by FUNCT_1:def 6;
consider x1, x2 being object such that
A10: x = [x1,x2] by A8, RELAT_1:def 1;
A11: x1 = x2 by A8, A10, RELAT_1:def 10;
then A12: x in dom f by A7, A10, FUNCT_4:42;
then (~ f) . (x1,x2) = f . (x1,x2) by A10, A11, FUNCT_4:def 2;
hence y in f .: (id A) by A8, A9, A10, A12, FUNCT_1:def 6; :: thesis: verum