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)) ) )

( ( 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)) ) )

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;( 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)) )

given y, z being object such that A5:
x = [z,y]
and ( 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;( 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

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

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

(g * (~ f)) . (z,y) = (g * f) . (y,z)

hence
~ (g * f) = g * (~ f)
by A1, FUNCT_4:def 2; :: thesis: verum(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;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