let f, g be Function; 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 ; ( 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):]
; ( 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 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 ;
( ( 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;
( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) )assume
x in f .: (proj1 X)
;
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;
verum end;
hence
proj1 ([:f,g:] .: X) = f .: (proj1 X)
by TARSKI:2; proj2 ([:f,g:] .: X) = g .: (proj2 X)
A8:
proj2 ([:f,g:] .: X) c= g .: (proj2 X)
by Th3;
now 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 ;
( ( 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;
( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) )assume
x in g .: (proj2 X)
;
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;
verum end;
hence
proj2 ([:f,g:] .: X) = g .: (proj2 X)
by TARSKI:2; verum