let B be set ; :: thesis: 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 ; :: thesis: for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C)
let f, g be Function; :: thesis: <: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 ; :: thesis: ( 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) ) :: thesis: ( x in (f " B) /\ (g " C) implies x in <:f,g:> " [:B,C:] )

proof

assume A1: x in <:f,g:> " [:B,C:] ; :: thesis: 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; :: thesis: verum

end;

assume A11: x in (f " B) /\ (g " C) ; :: thesis: 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; :: thesis: verum

end;

hence <:f,g:> " [:B,C:] = (f " B) /\ (g " C) by TARSKI:2; :: thesis: verum