let f, g be Function; :: thesis:
let X be set ; :: thesis:
assume A1: X c= [:(dom f),(dom g):] ; :: thesis:
A2: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 9;
A3: proj1 ([:f,g:] .: X) c= f .: (proj1 X) by Th3;
A4: proj2 ([:f,g:] .: X) c= g .: (proj2 X) by Th3;

let x be set ; :: thesis:
thus ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) by A3; :: thesis:
assume x in f .: (proj1 X) ; :: thesis:
then consider x' being set such that
A5: x' in dom f and
A6: x' in proj1 X and
A7: x = f . x' by FUNCT_1:def 12;
consider y' being set such that
A8: [x',y'] in X by A6, RELAT_1:def 4;
y' in dom g by A1, A8, ZFMISC_1:106;
then [:f,g:] . x',y' = [(f . x'),(g . y')] by A5, FUNCT_3:def 9;
then [x,(g . y')] in [:f,g:] .: X by A1, A2, A7, A8, FUNCT_1:def 12;
hence x in proj1 ([:f,g:] .: X) by RELAT_1:def 4; :: thesis:

end;

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

let x be set ; :: thesis:
thus ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) by A4; :: thesis:
assume x in g .: (proj2 X) ; :: thesis:
then consider x' being set such that
A9: x' in dom g and
A10: x' in proj2 X and
A11: x = g . x' by FUNCT_1:def 12;
consider y' being set such that
A12: [y',x'] in X by A10, RELAT_1:def 5;
y' in dom f by A1, A12, ZFMISC_1:106;
then [:f,g:] . y',x' = [(f . y'),(g . x')] by A9, FUNCT_3:def 9;
then [(f . y'),x] in [:f,g:] .: X by A1, A2, A11, A12, FUNCT_1:def 12;
hence x in proj2 ([:f,g:] .: X) by RELAT_1:def 5; :: thesis:

end;

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