let B be set ; for C being non empty set
for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C)
let C be non empty set ; for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C)
let f, g be Function; <:f,g:> " [:B,C:] = (f " B) /\ (g " C)
for x being object holds
( x in <:f,g:> " [:B,C:] iff x in (f " B) /\ (g " C) )
proof
let x be
object ;
( x in <:f,g:> " [:B,C:] iff x in (f " B) /\ (g " C) )
thus
(
x in <:f,g:> " [:B,C:] implies
x in (f " B) /\ (g " C) )
( x in (f " B) /\ (g " C) implies x in <:f,g:> " [:B,C:] )proof
assume A1:
x in <:f,g:> " [:B,C:]
;
x in (f " B) /\ (g " C)
then
<:f,g:> . x in [:B,C:]
by FUNCT_1:def 7;
then consider y1,
y2 being
object such that A2:
y1 in B
and A3:
y2 in C
and A4:
<:f,g:> . x = [y1,y2]
by ZFMISC_1:def 2;
A5:
x in dom <:f,g:>
by A1, FUNCT_1:def 7;
then A6:
x in (dom f) /\ (dom g)
by Def7;
then A7:
x in dom g
by XBOOLE_0:def 4;
A8:
[y1,y2] = [(f . x),(g . x)]
by A4, A5, Def7;
then
y2 = g . x
by XTUPLE_0:1;
then A9:
x in g " C
by A3, A7, FUNCT_1:def 7;
A10:
x in dom f
by A6, XBOOLE_0:def 4;
y1 = f . x
by A8, XTUPLE_0:1;
then
x in f " B
by A2, A10, FUNCT_1:def 7;
hence
x in (f " B) /\ (g " C)
by A9, XBOOLE_0:def 4;
verum
end;
assume A11:
x in (f " B) /\ (g " C)
;
x in <:f,g:> " [:B,C:]
then A12:
x in g " C
by XBOOLE_0:def 4;
then A13:
x in dom g
by FUNCT_1:def 7;
A14:
x in f " B
by A11, XBOOLE_0:def 4;
then
x in dom f
by FUNCT_1:def 7;
then A15:
x in (dom f) /\ (dom g)
by A13, XBOOLE_0:def 4;
then A16:
x in dom <:f,g:>
by Def7;
A17:
g . x in C
by A12, FUNCT_1:def 7;
f . x in B
by A14, FUNCT_1:def 7;
then
[(f . x),(g . x)] in [:B,C:]
by A17, ZFMISC_1:def 2;
then
<:f,g:> . x in [:B,C:]
by A15, Th48;
hence
x in <:f,g:> " [:B,C:]
by A16, FUNCT_1:def 7;
verum
end;
hence
<:f,g:> " [:B,C:] = (f " B) /\ (g " C)
by TARSKI:2; verum