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

A1: now :: thesis: for x being object holds

( ( x in dom ((~ f) * [:h,g:]) implies ex z1, y1 being object st

( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being object st

( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )

( ( x in dom ((~ f) * [:h,g:]) implies ex z1, y1 being object st

( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being object st

( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )

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

( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being object st

( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )

A8: [y,z] in dom (f * [:g,h:]) ; :: thesis: x in dom ((~ f) * [:h,g:])

A9: [:g,h:] . (y,z) in dom f by A8, FUNCT_1:11;

A10: dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 8;

[y,z] in dom [:g,h:] by A8, FUNCT_1:11;

then A11: ( y in dom g & z in dom h ) by A10, ZFMISC_1:87;

then ( [:g,h:] . (y,z) = [(g . y),(h . z)] & [:h,g:] . (z,y) = [(h . z),(g . y)] ) by FUNCT_3:def 8;

then A12: [:h,g:] . x in dom (~ f) by A7, A9, FUNCT_4:42;

dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def 8;

then x in dom [:h,g:] by A7, A11, ZFMISC_1:87;

hence x in dom ((~ f) * [:h,g:]) by A12, FUNCT_1:11; :: thesis: verum

end;( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being object st

( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )

hereby :: thesis: ( ex y, z being object st

( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) )

given y, z being object such that A7:
x = [z,y]
and ( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) )

assume A2:
x in dom ((~ f) * [:h,g:])
; :: thesis: ex z1, y1 being object st

( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )

then x in dom [:h,g:] by FUNCT_1:11;

then x in [:(dom h),(dom g):] by FUNCT_3:def 8;

then consider y1, z1 being object such that

A3: ( y1 in dom h & z1 in dom g ) and

A4: x = [y1,z1] by ZFMISC_1:84;

A5: ( [:h,g:] . (y1,z1) = [(h . y1),(g . z1)] & [:g,h:] . (z1,y1) = [(g . z1),(h . y1)] ) by A3, FUNCT_3:def 8;

[:h,g:] . (y1,z1) in dom (~ f) by A2, A4, FUNCT_1:11;

then A6: [:g,h:] . (z1,y1) in dom f by A5, FUNCT_4:42;

take z1 = z1; :: thesis: ex y1 being object st

( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )

take y1 = y1; :: thesis: ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )

thus x = [y1,z1] by A4; :: thesis: [z1,y1] in dom (f * [:g,h:])

dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 8;

then [z1,y1] in dom [:g,h:] by A3, ZFMISC_1:87;

hence [z1,y1] in dom (f * [:g,h:]) by A6, FUNCT_1:11; :: thesis: verum

end;( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )

then x in dom [:h,g:] by FUNCT_1:11;

then x in [:(dom h),(dom g):] by FUNCT_3:def 8;

then consider y1, z1 being object such that

A3: ( y1 in dom h & z1 in dom g ) and

A4: x = [y1,z1] by ZFMISC_1:84;

A5: ( [:h,g:] . (y1,z1) = [(h . y1),(g . z1)] & [:g,h:] . (z1,y1) = [(g . z1),(h . y1)] ) by A3, FUNCT_3:def 8;

[:h,g:] . (y1,z1) in dom (~ f) by A2, A4, FUNCT_1:11;

then A6: [:g,h:] . (z1,y1) in dom f by A5, FUNCT_4:42;

take z1 = z1; :: thesis: ex y1 being object st

( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )

take y1 = y1; :: thesis: ( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )

thus x = [y1,z1] by A4; :: thesis: [z1,y1] in dom (f * [:g,h:])

dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 8;

then [z1,y1] in dom [:g,h:] by A3, ZFMISC_1:87;

hence [z1,y1] in dom (f * [:g,h:]) by A6, FUNCT_1:11; :: thesis: verum

A8: [y,z] in dom (f * [:g,h:]) ; :: thesis: x in dom ((~ f) * [:h,g:])

A9: [:g,h:] . (y,z) in dom f by A8, FUNCT_1:11;

A10: dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 8;

[y,z] in dom [:g,h:] by A8, FUNCT_1:11;

then A11: ( y in dom g & z in dom h ) by A10, ZFMISC_1:87;

then ( [:g,h:] . (y,z) = [(g . y),(h . z)] & [:h,g:] . (z,y) = [(h . z),(g . y)] ) by FUNCT_3:def 8;

then A12: [:h,g:] . x in dom (~ f) by A7, A9, FUNCT_4:42;

dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def 8;

then x in dom [:h,g:] by A7, A11, ZFMISC_1:87;

hence x in dom ((~ f) * [:h,g:]) by A12, FUNCT_1:11; :: thesis: verum

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

((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)

hence
~ (f * [:g,h:]) = (~ f) * [:h,g:]
by A1, FUNCT_4:def 2; :: thesis: verum((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)

let y, z be object ; :: thesis: ( [y,z] in dom (f * [:g,h:]) implies ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z) )

assume A13: [y,z] in dom (f * [:g,h:]) ; :: thesis: ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)

then [y,z] in dom [:g,h:] by FUNCT_1:11;

then [y,z] in [:(dom g),(dom h):] by FUNCT_3:def 8;

then A14: ( y in dom g & z in dom h ) by ZFMISC_1:87;

[:g,h:] . (y,z) in dom f by A13, FUNCT_1:11;

then A15: [(g . y),(h . z)] in dom f by A14, FUNCT_3:def 8;

[z,y] in [:(dom h),(dom g):] by A14, ZFMISC_1:87;

then [z,y] in dom [:h,g:] by FUNCT_3:def 8;

hence ((~ f) * [:h,g:]) . (z,y) = (~ f) . ([:h,g:] . (z,y)) by FUNCT_1:13

.= (~ f) . ((h . z),(g . y)) by A14, FUNCT_3:def 8

.= f . ((g . y),(h . z)) by A15, FUNCT_4:def 2

.= f . ([:g,h:] . (y,z)) by A14, FUNCT_3:def 8

.= (f * [:g,h:]) . (y,z) by A13, FUNCT_1:12 ;

:: thesis: verum

end;assume A13: [y,z] in dom (f * [:g,h:]) ; :: thesis: ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)

then [y,z] in dom [:g,h:] by FUNCT_1:11;

then [y,z] in [:(dom g),(dom h):] by FUNCT_3:def 8;

then A14: ( y in dom g & z in dom h ) by ZFMISC_1:87;

[:g,h:] . (y,z) in dom f by A13, FUNCT_1:11;

then A15: [(g . y),(h . z)] in dom f by A14, FUNCT_3:def 8;

[z,y] in [:(dom h),(dom g):] by A14, ZFMISC_1:87;

then [z,y] in dom [:h,g:] by FUNCT_3:def 8;

hence ((~ f) * [:h,g:]) . (z,y) = (~ f) . ([:h,g:] . (z,y)) by FUNCT_1:13

.= (~ f) . ((h . z),(g . y)) by A14, FUNCT_3:def 8

.= f . ((g . y),(h . z)) by A15, FUNCT_4:def 2

.= f . ([:g,h:] . (y,z)) by A14, FUNCT_3:def 8

.= (f * [:g,h:]) . (y,z) by A13, FUNCT_1:12 ;

:: thesis: verum