let f, g be Function; :: thesis: ~ (g * f) = g * (~ f)

A1: now

let x be set ; :: thesis: ( ( x in dom (g * (~ f)) implies ex y1, z1 being set st
( x = [z1,y1] & [y1,z1] in dom (g * f) ) ) & ( ex y, z being set st
( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) ) )

hereby :: thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) )

assume A2: x in dom (g * (~ f)) ; :: thesis: ex y1, z1 being set st
( x = [z1,y1] & [y1,z1] in dom (g * f) )
then x in dom (~ f) by FUNCT_1:21;
then consider y1, z1 being set such that
A3: x = [z1,y1] and
A4: [y1,z1] in dom f by FUNCT_4:def 2;
take y1 = y1; :: thesis: ex z1 being set st
( x = [z1,y1] & [y1,z1] in dom (g * f) )
take z1 = z1; :: thesis: ( x = [z1,y1] & [y1,z1] in dom (g * f) )
thus x = [z1,y1] by A3; :: thesis: [y1,z1] in dom (g * f)
(~ f) . z1,y1 in dom g by A2, A3, FUNCT_1:21;
then f . y1,z1 in dom g by A4, FUNCT_4:def 2;
hence [y1,z1] in dom (g * f) by A4, FUNCT_1:21; :: thesis: verum

end;

given y, z being set such that A5: x = [z,y] and
A6: [y,z] in dom (g * f) ; :: thesis: x in dom (g * (~ f))
A7: [y,z] in dom f by A6, FUNCT_1:21;
f . y,z in dom g by A6, FUNCT_1:21;
then A8: (~ f) . z,y in dom g by A7, FUNCT_4:def 2;
x in dom (~ f) by A5, A7, FUNCT_4:def 2;
hence x in dom (g * (~ f)) by A5, A8, FUNCT_1:21; :: thesis: verum

end;

now

let y, z be set ; :: thesis: ( [y,z] in dom (g * f) implies (g * (~ f)) . z,y = (g * f) . y,z )
assume A9: [y,z] in dom (g * f) ; :: thesis: (g * (~ f)) . z,y = (g * f) . y,z
then [y,z] in dom f by FUNCT_1:21;
then A10: [z,y] in dom (~ f) by FUNCT_4:43;
hence (g * (~ f)) . z,y = g . ((~ f) . z,y) by FUNCT_1:23
.= g . (f . y,z) by A10, FUNCT_4:44
.= (g * f) . y,z by A9, FUNCT_1:22 ;
:: thesis: verum

end;

hence ~ (g * f) = g * (~ f) by A1, FUNCT_4:def 2; :: thesis: verum