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 ;
[:h,g:] . (y1,z1) in dom (~ f) by ;
then A6: [:g,h:] . (z1,y1) in dom f by ;
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 ;
hence [z1,y1] in dom (f * [:g,h:]) by ; :: 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 ;
A10: dom [:g,h:] = [:(dom g),(dom h):] by FUNCT_3:def 8;
[y,z] in dom [:g,h:] by ;
then A11: ( y in dom g & z in dom h ) by ;
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 ;
dom [:h,g:] = [:(dom h),(dom g):] by FUNCT_3:def 8;
then x in dom [:h,g:] by ;
hence x in dom ((~ f) * [:h,g:]) by ; :: 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 ;
then A15: [(g . y),(h . z)] in dom f by ;
[z,y] in [:(dom h),(dom g):] by ;
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
.= f . ((g . y),(h . z)) by
.= f . ([:g,h:] . (y,z)) by
.= (f * [:g,h:]) . (y,z) by ;
:: thesis: verum
end;
hence ~ (f * [:g,h:]) = (~ f) * [:h,g:] by ; :: thesis: verum