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

A1: now :: thesis: for x being object holds
( ( x in dom (g * (~ f)) implies ex y1, z1 being object st
( x = [z1,y1] & [y1,z1] in dom (g * f) ) ) & ( ex y, z being object st
( x = [z,y] & [y,z] in dom (g * f) ) implies x in dom (g * (~ f)) ) )

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

hereby :: thesis: ( ex y, z being object 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 object st
( x = [z1,y1] & [y1,z1] in dom (g * f) )
then x in dom (~ f) by FUNCT_1:11;
then consider y1, z1 being object 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 object 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:11;
then f . (y1,z1) in dom g by A4, FUNCT_4:def 2;
hence [y1,z1] in dom (g * f) by A4, FUNCT_1:11; :: thesis: verum

end;

given y, z being object 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:11;
then A8: x in dom (~ f) by A5, FUNCT_4:def 2;
f . (y,z) in dom g by A6, FUNCT_1:11;
then (~ f) . (z,y) in dom g by A7, FUNCT_4:def 2;
hence x in dom (g * (~ f)) by A5, A8, FUNCT_1:11; :: thesis: verum

end;

now :: thesis: for y, z being object st [y,z] in dom (g * f) holds
(g * (~ f)) . (z,y) = (g * f) . (y,z)

let y, z be object ; :: 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:11;
then A10: [z,y] in dom (~ f) by FUNCT_4:42;
hence (g * (~ f)) . (z,y) = g . ((~ f) . (z,y)) by FUNCT_1:13
.= g . (f . (y,z)) by A10, FUNCT_4:43
.= (g * f) . (y,z) by A9, FUNCT_1:12 ;
:: thesis: verum

end;

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