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 8;
A5: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 8;
A6: dom [:g,f:] = [:(dom g),(dom f):] by FUNCT_3:def 8;
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:46
.= dom [:(f "),(g "):] by FUNCT_3:def 8
.= rng [:f,g:] by A8, A10, FUNCT_1:32
.= rng (~ [:f,g:]) by A5, FUNCT_4:47 ;

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:47;
then y in [:(rng f),(rng g):] by FUNCT_3:67;
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:84;
set x1 = (f ") . y1;
set x2 = (g ") . y2;
A17: y2 in dom (g ") by A2, A15, FUNCT_1:32;
A18: y1 in dom (f ") by A1, A14, FUNCT_1:32;
then [y2,y1] in dom ([:g,f:] ") by A4, A17, ZFMISC_1:87;
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 8 ;
A20: y1 in dom (f ") by A1, A14, FUNCT_1:32;
A21: y2 in dom (g ") by A2, A15, FUNCT_1:32;
A22: (f ") . y1 in rng (f ") by A20, FUNCT_1:def 3;
A23: (g ") . y2 in rng (g ") by A21, FUNCT_1:def 3;
A24: (f ") . y1 in dom f by A1, A22, FUNCT_1:33;
A25: (g ") . y2 in dom g by A2, A23, FUNCT_1:33;
then A26: [((g ") . y2),((f ") . y1)] in dom [:g,f:] by A6, A24, ZFMISC_1:87;
then A27: [((g ") . y2),((f ") . y1)] in dom (~ [:f,g:]) by A5, A6, FUNCT_4:46;
thus x in dom (~ [:f,g:]) by A5, A6, A13, A16, A19, A26, FUNCT_4:46; :: thesis: (~ [:f,g:]) . x = y
A28: f . ((f ") . y1) = y1 by A1, A14, FUNCT_1:32;
A29: g . ((g ") . y2) = y2 by A2, A15, FUNCT_1:32;
thus (~ [:f,g:]) . x = (~ [:f,g:]) . (((g ") . y2),((f ") . y1)) by A13, A16, A19
.= [:f,g:] . (((f ") . y1),((g ") . y2)) by A27, FUNCT_4:43
.= y by A16, A24, A25, A28, A29, FUNCT_3:def 8 ; :: 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 3; :: thesis: x = (~ ([:g,f:] ")) . y
x in dom [:g,f:] by A5, A6, A30, FUNCT_4:46;
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:84;
A35: (~ [:f,g:]) . (x1,x2) = [:f,g:] . (x2,x1) by A30, A34, FUNCT_4:43
.= [(f . x2),(g . x1)] by A32, A33, FUNCT_3:def 8 ;
A36: g . x1 in rng g by A32, FUNCT_1:def 3;
f . x2 in rng f by A33, FUNCT_1:def 3;
then [(g . x1),(f . x2)] in [:(rng g),(rng f):] by A36, ZFMISC_1:87;
then [(g . x1),(f . x2)] in rng [:g,f:] by FUNCT_3:67;
then A37: [(g . x1),(f . x2)] in dom ([:g,f:] ") by A7, FUNCT_1:33;
[x1,x2] in dom [:g,f:] by A6, A32, A33, ZFMISC_1:87;
hence x = ([:g,f:] ") . ([:g,f:] . (x1,x2)) by A7, A34, FUNCT_1:34
.= ([:g,f:] ") . ((g . x1),(f . x2)) by A32, A33, FUNCT_3:def 8
.= (~ ([: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:32; :: thesis: verum