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 and
A4: z1 in dom g and
A5: x = [y1,z1] by ZFMISC_1:103;
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 A5; :: thesis: [z1,y1] in dom (f * [:g,h:])
dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 9;
then A6: [z1,y1] in dom [:g,h:] by A3, A4, ZFMISC_1:106;
A7: [:h,g:] . y1,z1 = [(h . y1),(g . z1)] by A3, A4, FUNCT_3:def 9;
A8: [:g,h:] . z1,y1 = [(g . z1),(h . y1)] by A3, A4, FUNCT_3:def 9;
[:h,g:] . y1,z1 in dom (~ f) by A2, A5, FUNCT_1:21;
then [:g,h:] . z1,y1 in dom f by A7, A8, FUNCT_4:43;
hence [z1,y1] in dom (f * [:g,h:]) by A6, FUNCT_1:21; :: thesis: verum

end;

given y, z being set such that A9: x = [z,y] and
A10: [y,z] in dom (f * [:g,h:]) ; :: thesis: x in dom ((~ f) * [:h,g:])
A11: [y,z] in dom [:g,h:] by A10, FUNCT_1:21;
dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 9;
then A12: ( y in dom g & z in dom h ) by A11, ZFMISC_1:106;
dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def 9;
then A13: x in dom [:h,g:] by A9, A12, ZFMISC_1:106;
A14: [:g,h:] . y,z = [(g . y),(h . z)] by A12, FUNCT_3:def 9;
A15: [:h,g:] . z,y = [(h . z),(g . y)] by A12, FUNCT_3:def 9;
[:g,h:] . y,z in dom f by A10, FUNCT_1:21;
then [:h,g:] . x in dom (~ f) by A9, A14, A15, FUNCT_4:43;
hence x in dom ((~ f) * [:h,g:]) by A13, 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 A16: [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 A17: ( y in dom g & z in dom h ) by ZFMISC_1:106;
[:g,h:] . y,z in dom f by A16, FUNCT_1:21;
then A18: [(g . y),(h . z)] in dom f by A17, FUNCT_3:def 9;
[z,y] in [:(dom h),(dom g):] by A17, 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 A17, FUNCT_3:def 9
.= f . (g . y),(h . z) by A18, FUNCT_4:def 2
.= f . ([:g,h:] . y,z) by A17, FUNCT_3:def 9
.= (f * [:g,h:]) . y,z by A16, FUNCT_1:22 ;
:: thesis: verum

end;

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