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 & y' in dom g & xy = [x',y'] ) by A1, A3, ZFMISC_1:def 2;
[x,y] = [:f,g:] . x',y' by A5, A6
.= [(f . x'),(g . y')] by A6, FUNCT_3:def 9 ;
then A7: x = f . x' by ZFMISC_1:33;
x' in proj1 X by A4, A6, RELAT_1:def 4;
hence x in f .: (proj1 X) by A6, A7, 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
A8: [x,y] in [:f,g:] .: X by RELAT_1:def 5;
consider xy being set such that
A9: xy in dom [:f,g:] and
A10: xy in X and
A11: [x,y] = [:f,g:] . xy by A8, FUNCT_1:def 12;
consider x', y' being set such that
A12: ( x' in dom f & y' in dom g & xy = [x',y'] ) by A1, A9, ZFMISC_1:def 2;
[x,y] = [:f,g:] . x',y' by A11, A12
.= [(f . x'),(g . y')] by A12, FUNCT_3:def 9 ;
then A13: y = g . y' by ZFMISC_1:33;
y' in proj2 X by A10, A12, RELAT_1:def 5;
hence y in g .: (proj2 X) by A12, A13, FUNCT_1:def 12; :: thesis: verum