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

proof

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

end;

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