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 " ) by A2, A15, FUNCT_1:54;
A18: y1 in dom (f " ) by A1, A14, FUNCT_1:54;
then [y2,y1] in dom ([:g,f:] " ) by A4, A17, ZFMISC_1:106;
then A19: (~ ([:g,f:] " )) . y1,y2 = [:(g " ),(f " ):] . y2,y1 by A3, FUNCT_4:def 2
.= [((g " ) . y2),((f " ) . y1)] by A17, A18, FUNCT_3:def 9 ;
A20: y1 in dom (f " ) by A1, A14, FUNCT_1:54;
A21: y2 in dom (g " ) by A2, A15, FUNCT_1:54;
A22: (f " ) . y1 in rng (f " ) by A20, FUNCT_1:def 5;
A23: (g " ) . y2 in rng (g " ) by A21, FUNCT_1:def 5;
A24: (f " ) . y1 in dom f by A1, A22, FUNCT_1:55;
A25: (g " ) . y2 in dom g by A2, A23, FUNCT_1:55;
then A26: [((g " ) . y2),((f " ) . y1)] in dom [:g,f:] by A6, A24, ZFMISC_1:106;
then A27: [((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, A19, A26, FUNCT_4:47; :: thesis: (~ [:f,g:]) . x = y
A28: f . ((f " ) . y1) = y1 by A1, A14, FUNCT_1:54;
A29: g . ((g " ) . y2) = y2 by A2, A15, FUNCT_1:54;
thus (~ [:f,g:]) . x = (~ [:f,g:]) . ((g " ) . y2),((f " ) . y1) by A13, A16, A19
.= [:f,g:] . ((f " ) . y1),((g " ) . y2) by A27, FUNCT_4:44
.= y by A16, A24, A25, A28, A29, FUNCT_3:def 9 ; :: thesis: verum

end;

assume that
A30: x in dom (~ [:f,g:]) and
A31: (~ [:f,g:]) . x = y ; :: thesis: ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] " )) . y )
thus y in rng (~ [:f,g:]) by A30, A31, FUNCT_1:def 5; :: thesis: x = (~ ([:g,f:] " )) . y
x in dom [:g,f:] by A5, A6, A30, FUNCT_4:47;
then consider x1, x2 being set such that
A32: x1 in dom g and
A33: x2 in dom f and
A34: x = [x1,x2] by A6, ZFMISC_1:103;
A35: (~ [:f,g:]) . x1,x2 = [:f,g:] . x2,x1 by A30, A34, FUNCT_4:44
.= [(f . x2),(g . x1)] by A32, A33, FUNCT_3:def 9 ;
A36: g . x1 in rng g by A32, FUNCT_1:def 5;
f . x2 in rng f by A33, FUNCT_1:def 5;
then [(g . x1),(f . x2)] in [:(rng g),(rng f):] by A36, ZFMISC_1:106;
then [(g . x1),(f . x2)] in rng [:g,f:] by FUNCT_3:88;
then A37: [(g . x1),(f . x2)] in dom ([:g,f:] " ) by A7, FUNCT_1:55;
[x1,x2] in dom [:g,f:] by A6, A32, A33, ZFMISC_1:106;
hence x = ([:g,f:] " ) . ([:g,f:] . x1,x2) by A7, A34, FUNCT_1:56
.= ([:g,f:] " ) . (g . x1),(f . x2) by A32, A33, FUNCT_3:def 9
.= (~ ([:g,f:] " )) . (f . x2),(g . x1) by A37, FUNCT_4:def 2
.= (~ ([:g,f:] " )) . y by A31, A34, A35 ;
:: thesis: verum

end;

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