let f, g be Function; ( dom f = dom g implies pr1 <:f,g:> = f )
assume A1:
dom f = dom g
; 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 ;
( x in dom (pr1 <:f,g:>) implies (pr1 <:f,g:>) . x = f . x )
assume A4:
x in dom (pr1 <:f,g:>)
;
(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
;
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; verum