let f, g be Function; :: thesis: ( f is one-to-one & g is one-to-one implies (~ [:f,g:]) " = ~ ([:g,f:] " ) )
assume that
A1: f is one-to-one and
A2: g is one-to-one ; :: thesis: (~ [:f,g:]) " = ~ ([:g,f:] " )
A3: [:g,f:] " = [:(g " ),(f " ):] by A1, A2, Th7;
then A4: dom ([:g,f:] " ) = [:(dom (g " )),(dom (f " )):] by FUNCT_3:def 9;
A5: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 9;
A6: dom [:g,f:] = [:(dom g),(dom f):] by FUNCT_3:def 9;
A7: [:g,f:] is one-to-one by A1, A2, ISOCAT_1:1;
A8: [:f,g:] is one-to-one by A1, A2, ISOCAT_1:1;
then A9: ~ [:f,g:] is one-to-one by Th9;
A10: [:f,g:] " = [:(f " ),(g " ):] by A1, A2, Th7;
A11: dom (~ ([:g,f:] " )) = [:(dom (f " )),(dom (g " )):] by A4, FUNCT_4:47
.= dom [:(f " ),(g " ):] by FUNCT_3:def 9
.= rng [:f,g:] by A8, A10, FUNCT_1:54
.= rng (~ [:f,g:]) by A5, FUNCT_4:48 ;

now

let y, x be set ; :: thesis: ( ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] " )) . y implies ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y ) ) & ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] " )) . y ) ) )

hereby :: thesis: ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] " )) . y ) )

assume that
A12: y in rng (~ [:f,g:]) and
A13: x = (~ ([:g,f:] " )) . y ; :: thesis: ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y )
y in rng [:f,g:] by A5, A12, FUNCT_4:48;
then y in [:(rng f),(rng g):] by FUNCT_3:88;
then consider y1, y2 being set such that
A14: y1 in rng f and
A15: y2 in rng g and
A16: y = [y1,y2] by ZFMISC_1:103;
set x1 = (f " ) . y1;
set x2 = (g " ) . y2;
A17: ( y2 in dom (g " ) & y1 in dom (f " ) ) by A1, A2, A14, A15, FUNCT_1:54;
then [y2,y1] in dom ([:g,f:] " ) by A4, ZFMISC_1:106;
then A18: (~ ([:g,f:] " )) . y1,y2 = [:(g " ),(f " ):] . y2,y1 by A3, FUNCT_4:def 2
.= [((g " ) . y2),((f " ) . y1)] by A17, FUNCT_3:def 9 ;
( y1 in dom (f " ) & y2 in dom (g " ) ) by A1, A2, A14, A15, FUNCT_1:54;
then ( (f " ) . y1 in rng (f " ) & (g " ) . y2 in rng (g " ) ) by FUNCT_1:def 5;
then A19: ( (f " ) . y1 in dom f & (g " ) . y2 in dom g ) by A1, A2, FUNCT_1:55;
then A20: [((g " ) . y2),((f " ) . y1)] in dom [:g,f:] by A6, ZFMISC_1:106;
then A21: [((g " ) . y2),((f " ) . y1)] in dom (~ [:f,g:]) by A5, A6, FUNCT_4:47;
thus x in dom (~ [:f,g:]) by A5, A6, A13, A16, A18, A20, FUNCT_4:47; :: thesis: (~ [:f,g:]) . x = y
A22: ( f . ((f " ) . y1) = y1 & g . ((g " ) . y2) = y2 ) by A1, A2, A14, A15, FUNCT_1:54;
thus (~ [:f,g:]) . x = (~ [:f,g:]) . ((g " ) . y2),((f " ) . y1) by A13, A16, A18
.= [:f,g:] . ((f " ) . y1),((g " ) . y2) by A21, FUNCT_4:44
.= y by A16, A19, A22, FUNCT_3:def 9 ; :: thesis: verum

end;

assume that
A23: x in dom (~ [:f,g:]) and
A24: (~ [:f,g:]) . x = y ; :: thesis: ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] " )) . y )
thus y in rng (~ [:f,g:]) by A23, A24, FUNCT_1:def 5; :: thesis: x = (~ ([:g,f:] " )) . y
x in dom [:g,f:] by A5, A6, A23, FUNCT_4:47;
then consider x1, x2 being set such that
A25: x1 in dom g and
A26: x2 in dom f and
A27: x = [x1,x2] by A6, ZFMISC_1:103;
A28: (~ [:f,g:]) . x1,x2 = [:f,g:] . x2,x1 by A23, A27, FUNCT_4:44
.= [(f . x2),(g . x1)] by A25, A26, FUNCT_3:def 9 ;
( g . x1 in rng g & f . x2 in rng f ) by A25, A26, FUNCT_1:def 5;
then [(g . x1),(f . x2)] in [:(rng g),(rng f):] by ZFMISC_1:106;
then [(g . x1),(f . x2)] in rng [:g,f:] by FUNCT_3:88;
then A29: [(g . x1),(f . x2)] in dom ([:g,f:] " ) by A7, FUNCT_1:55;
[x1,x2] in dom [:g,f:] by A6, A25, A26, ZFMISC_1:106;
hence x = ([:g,f:] " ) . ([:g,f:] . x1,x2) by A7, A27, FUNCT_1:56
.= ([:g,f:] " ) . (g . x1),(f . x2) by A25, A26, FUNCT_3:def 9
.= (~ ([:g,f:] " )) . (f . x2),(g . x1) by A29, FUNCT_4:def 2
.= (~ ([:g,f:] " )) . y by A24, A27, A28 ;
:: thesis: verum

end;

hence (~ [:f,g:]) " = ~ ([:g,f:] " ) by A9, A11, FUNCT_1:54; :: thesis: verum