let A be set ; :: thesis: for f, g being Function holds <:f,g:> .: A c= [:(f .: A),(g .: A):]
let f, g be Function; :: thesis: <:f,g:> .: A c= [:(f .: A),(g .: A):]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in <:f,g:> .: A or y in [:(f .: A),(g .: A):] )
assume y in <:f,g:> .: A ; :: thesis: y in [:(f .: A),(g .: A):]
then consider x being object such that
A1: x in dom <:f,g:> and
A2: x in A and
A3: y = <:f,g:> . x by FUNCT_1:def 6;
A4: x in (dom f) /\ (dom g) by A1, Def7;
then x in dom f by XBOOLE_0:def 4;
then A5: f . x in f .: A by A2, FUNCT_1:def 6;
x in dom g by A4, XBOOLE_0:def 4;
then A6: g . x in g .: A by A2, FUNCT_1:def 6;
y = [(f . x),(g . x)] by A1, A3, Def7;
hence y in [:(f .: A),(g .: A):] by A5, A6, ZFMISC_1:def 2; :: thesis: verum