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: dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def 8
.= dom f by A1 ;
for x being set st x in dom (pr1 <:f,g:>) holds
(pr1 <:f,g:>) . x = f . x

proof

let x be set ; :: 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 8
.= f . x by MCART_1:def 1 ; :: thesis: verum

end;

hence pr1 <:f,g:> = f by A2, A3, FUNCT_1:9; :: thesis: verum