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 ;
then f . (y1,z1) in dom g by ;
hence [y1,z1] in dom (g * f) by ; :: 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 ;
then A8: x in dom (~ f) by ;
f . (y,z) in dom g by ;
then (~ f) . (z,y) in dom g by ;
hence x in dom (g * (~ f)) by ; :: 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
.= (g * f) . (y,z) by ;
:: thesis: verum
end;
hence ~ (g * f) = g * (~ f) by ; :: thesis: verum