let f, g be Function; :: thesis: for X being set holds
( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )
let X be set ; :: thesis: ( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )
A1: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 9;

hereby :: according to TARSKI:def 3 :: thesis: proj2 ([:f,g:] .: X) c= g .: (proj2 X)

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

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 ([:f,g:] .: X) or y in g .: (proj2 X) )
assume y in proj2 ([:f,g:] .: X) ; :: thesis: y in g .: (proj2 X)
then consider x being set such that
A10: [x,y] in [:f,g:] .: X by RELAT_1:def 5;
consider xy being set such that
A11: xy in dom [:f,g:] and
A12: xy in X and
A13: [x,y] = [:f,g:] . xy by A10, FUNCT_1:def 12;
consider x', y' being set such that
A14: x' in dom f and
A15: y' in dom g and
A16: xy = [x',y'] by A1, A11, ZFMISC_1:def 2;
[x,y] = [:f,g:] . x',y' by A13, A16
.= [(f . x'),(g . y')] by A14, A15, FUNCT_3:def 9 ;
then A17: y = g . y' by ZFMISC_1:33;
y' in proj2 X by A12, A16, RELAT_1:def 5;
hence y in g .: (proj2 X) by A15, A17, FUNCT_1:def 12; :: thesis: verum