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

A1: now

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

hereby :: thesis: ( ex y, z being set 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 set st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )
then x in dom [:h,g:] by FUNCT_1:21;
then x in [:(dom h),(dom g):] by FUNCT_3:def 9;
then consider y1, z1 being set such that
A3: ( y1 in dom h & z1 in dom g ) and
A4: x = [y1,z1] by ZFMISC_1:103;
A5: ( [:h,g:] . y1,z1 = [(h . y1),(g . z1)] & [:g,h:] . z1,y1 = [(g . z1),(h . y1)] ) by A3, FUNCT_3:def 9;
[:h,g:] . y1,z1 in dom (~ f) by A2, A4, FUNCT_1:21;
then A6: [:g,h:] . z1,y1 in dom f by A5, FUNCT_4:43;
take z1 = z1; :: thesis: ex y1 being set 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 9;
then [z1,y1] in dom [:g,h:] by A3, ZFMISC_1:106;
hence [z1,y1] in dom (f * [:g,h:]) by A6, FUNCT_1:21; :: thesis: verum

end;

given y, z being set 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:21;
A10: dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 9;
[y,z] in dom [:g,h:] by A8, FUNCT_1:21;
then A11: ( y in dom g & z in dom h ) by A10, ZFMISC_1:106;
then ( [:g,h:] . y,z = [(g . y),(h . z)] & [:h,g:] . z,y = [(h . z),(g . y)] ) by FUNCT_3:def 9;
then A12: [:h,g:] . x in dom (~ f) by A7, A9, FUNCT_4:43;
dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def 9;
then x in dom [:h,g:] by A7, A11, ZFMISC_1:106;
hence x in dom ((~ f) * [:h,g:]) by A12, FUNCT_1:21; :: thesis: verum

end;

now

let y, z be set ; :: 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:21;
then [y,z] in [:(dom g),(dom h):] by FUNCT_3:def 9;
then A14: ( y in dom g & z in dom h ) by ZFMISC_1:106;
[:g,h:] . y,z in dom f by A13, FUNCT_1:21;
then A15: [(g . y),(h . z)] in dom f by A14, FUNCT_3:def 9;
[z,y] in [:(dom h),(dom g):] by A14, ZFMISC_1:106;
then [z,y] in dom [:h,g:] by FUNCT_3:def 9;
hence ((~ f) * [:h,g:]) . z,y = (~ f) . ([:h,g:] . z,y) by FUNCT_1:23
.= (~ f) . (h . z),(g . y) by A14, FUNCT_3:def 9
.= f . (g . y),(h . z) by A15, FUNCT_4:def 2
.= f . ([:g,h:] . y,z) by A14, FUNCT_3:def 9
.= (f * [:g,h:]) . y,z by A13, FUNCT_1:22 ;
:: thesis: verum

end;

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