let f, g be Function; :: thesis: for X being set st X c= [:(dom f),(dom g):] holds
( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )
let X be set ; :: thesis: ( X c= [:(dom f),(dom g):] implies ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) )
assume A1: X c= [:(dom f),(dom g):] ; :: thesis: ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )
A2: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 8;
A3: proj1 ([:f,g:] .: X) c= f .: (proj1 X) by Th3;

now :: thesis: for x being object holds
( ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) & ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) ) )

let x be object ; :: thesis: ( ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) & ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) ) )
thus ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) by A3; :: thesis: ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) )
assume x in f .: (proj1 X) ; :: thesis: x in proj1 ([:f,g:] .: X)
then consider x9 being object such that
A4: x9 in dom f and
A5: x9 in proj1 X and
A6: x = f . x9 by FUNCT_1:def 6;
consider y9 being object such that
A7: [x9,y9] in X by A5, XTUPLE_0:def 12;
y9 in dom g by A1, A7, ZFMISC_1:87;
then [:f,g:] . (x9,y9) = [(f . x9),(g . y9)] by A4, FUNCT_3:def 8;
then [x,(g . y9)] in [:f,g:] .: X by A1, A2, A6, A7, FUNCT_1:def 6;
hence x in proj1 ([:f,g:] .: X) by XTUPLE_0:def 12; :: thesis: verum

end;

hence proj1 ([:f,g:] .: X) = f .: (proj1 X) by TARSKI:2; :: thesis: proj2 ([:f,g:] .: X) = g .: (proj2 X)
A8: proj2 ([:f,g:] .: X) c= g .: (proj2 X) by Th3;

now :: thesis: for x being object holds
( ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) & ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) ) )

let x be object ; :: thesis: ( ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) & ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) ) )
thus ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) by A8; :: thesis: ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) )
assume x in g .: (proj2 X) ; :: thesis: x in proj2 ([:f,g:] .: X)
then consider x9 being object such that
A9: x9 in dom g and
A10: x9 in proj2 X and
A11: x = g . x9 by FUNCT_1:def 6;
consider y9 being object such that
A12: [y9,x9] in X by A10, XTUPLE_0:def 13;
y9 in dom f by A1, A12, ZFMISC_1:87;
then [:f,g:] . (y9,x9) = [(f . y9),(g . x9)] by A9, FUNCT_3:def 8;
then [(f . y9),x] in [:f,g:] .: X by A1, A2, A11, A12, FUNCT_1:def 6;
hence x in proj2 ([:f,g:] .: X) by XTUPLE_0:def 13; :: thesis: verum

end;

hence proj2 ([:f,g:] .: X) = g .: (proj2 X) by TARSKI:2; :: thesis: verum