let f, g be Function; 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 ; ( 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 8;
hereby TARSKI:def 3 proj2 ([:f,g:] .: X) c= g .: (proj2 X)
let x be
object ;
( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) )assume
x in proj1 ([:f,g:] .: X)
;
x in f .: (proj1 X)then consider y being
object such that A2:
[x,y] in [:f,g:] .: X
by XTUPLE_0:def 12;
consider xy being
object 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 6;
consider x9,
y9 being
object such that A6:
x9 in dom f
and A7:
y9 in dom g
and A8:
xy = [x9,y9]
by A1, A3, ZFMISC_1:def 2;
[x,y] =
[:f,g:] . (
x9,
y9)
by A5, A8
.=
[(f . x9),(g . y9)]
by A6, A7, FUNCT_3:def 8
;
then A9:
x = f . x9
by XTUPLE_0:1;
x9 in proj1 X
by A4, A8, XTUPLE_0:def 12;
hence
x in f .: (proj1 X)
by A6, A9, FUNCT_1:def 6;
verum
end;
let y be object ; TARSKI:def 3 ( not y in proj2 ([:f,g:] .: X) or y in g .: (proj2 X) )
assume
y in proj2 ([:f,g:] .: X)
; y in g .: (proj2 X)
then consider x being object such that
A10:
[x,y] in [:f,g:] .: X
by XTUPLE_0:def 13;
consider xy being object 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 6;
consider x9, y9 being object such that
A14:
x9 in dom f
and
A15:
y9 in dom g
and
A16:
xy = [x9,y9]
by A1, A11, ZFMISC_1:def 2;
[x,y] =
[:f,g:] . (x9,y9)
by A13, A16
.=
[(f . x9),(g . y9)]
by A14, A15, FUNCT_3:def 8
;
then A17:
y = g . y9
by XTUPLE_0:1;
y9 in proj2 X
by A12, A16, XTUPLE_0:def 13;
hence
y in g .: (proj2 X)
by A15, A17, FUNCT_1:def 6; verum