let Y, Z be set ; :: thesis: for f, g being Function st dom f = dom g & rng f c= Y & rng g c= Z holds
( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g )
let f, g be Function; :: thesis: ( dom f = dom g & rng f c= Y & rng g c= Z implies ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g ) )
assume that
A1: dom f = dom g and
A2: ( rng f c= Y & rng g c= Z ) ; :: thesis: ( (pr1 (Y,Z)) * <:f,g:> = f & (pr2 (Y,Z)) * <:f,g:> = g )
A3: [:(rng f),(rng g):] c= [:Y,Z:] by A2, ZFMISC_1:96;
A4: rng <:f,g:> c= [:(rng f),(rng g):] by Th51;
dom (pr1 (Y,Z)) = [:Y,Z:] by Def4;
then A5: dom ((pr1 (Y,Z)) * <:f,g:>) = dom <:f,g:> by A3, A4, RELAT_1:27, XBOOLE_1:1;
then A6: dom ((pr1 (Y,Z)) * <:f,g:>) = dom f by A1, Th50;
for x being object st x in dom f holds
((pr1 (Y,Z)) * <:f,g:>) . x = f . x

proof

let x be object ; :: thesis: ( x in dom f implies ((pr1 (Y,Z)) * <:f,g:>) . x = f . x )
assume A7: x in dom f ; :: thesis: ((pr1 (Y,Z)) * <:f,g:>) . x = f . x
then A8: ( f . x in rng f & g . x in rng g ) by A1, FUNCT_1:def 3;
thus ((pr1 (Y,Z)) * <:f,g:>) . x = (pr1 (Y,Z)) . (<:f,g:> . x) by A6, A7, FUNCT_1:12
.= (pr1 (Y,Z)) . ((f . x),(g . x)) by A5, A6, A7, Def7
.= f . x by A2, A8, Def4 ; :: thesis: verum

end;

hence (pr1 (Y,Z)) * <:f,g:> = f by A6; :: thesis: (pr2 (Y,Z)) * <:f,g:> = g
dom (pr2 (Y,Z)) = [:Y,Z:] by Def5;
then A9: dom ((pr2 (Y,Z)) * <:f,g:>) = dom <:f,g:> by A3, A4, RELAT_1:27, XBOOLE_1:1;
then A10: dom ((pr2 (Y,Z)) * <:f,g:>) = dom g by A1, Th50;
for x being object st x in dom g holds
((pr2 (Y,Z)) * <:f,g:>) . x = g . x

proof

let x be object ; :: thesis: ( x in dom g implies ((pr2 (Y,Z)) * <:f,g:>) . x = g . x )
assume A11: x in dom g ; :: thesis: ((pr2 (Y,Z)) * <:f,g:>) . x = g . x
then A12: ( f . x in rng f & g . x in rng g ) by A1, FUNCT_1:def 3;
thus ((pr2 (Y,Z)) * <:f,g:>) . x = (pr2 (Y,Z)) . (<:f,g:> . x) by A10, A11, FUNCT_1:12
.= (pr2 (Y,Z)) . ((f . x),(g . x)) by A9, A10, A11, Def7
.= g . x by A2, A12, Def5 ; :: thesis: verum

end;

hence (pr2 (Y,Z)) * <:f,g:> = g by A10; :: thesis: verum