let f, g be Function; :: thesis: ( dom f = dom g implies pr2 <:f,g:> = g )
assume A1: dom f = dom g ; :: thesis: pr2 <:f,g:> = g
A2: dom (pr2 <:f,g:>) = dom <:f,g:> by MCART_1:def 13;
A3: for x being object st x in dom (pr2 <:f,g:>) holds
(pr2 <:f,g:>) . x = g . x

proof

let x be object ; :: thesis: ( x in dom (pr2 <:f,g:>) implies (pr2 <:f,g:>) . x = g . x )
assume A4: x in dom (pr2 <:f,g:>) ; :: thesis: (pr2 <:f,g:>) . x = g . x
thus (pr2 <:f,g:>) . x = (<:f,g:> . x) `2 by A2, A4, MCART_1:def 13
.= [(f . x),(g . x)] `2 by A2, A4, FUNCT_3:def 7
.= g . x ; :: thesis: verum

end;

dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def 7
.= dom g by A1 ;
hence pr2 <:f,g:> = g by A2, A3; :: thesis: verum