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

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

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

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;

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

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)

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;

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