let f, g, h, k be Function; ( dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> implies ( f = k & g = h ) )
assume that
A1:
dom f = dom g
and
A2:
dom k = dom h
and
A3:
<:f,g:> = <:k,h:>
; ( f = k & g = h )
A4:
dom <:f,g:> = dom f
by A1, Th50;
for x being object st x in dom f holds
f . x = k . x
hence
f = k
by A2, A3, A4, Th50; g = h
A5:
dom <:f,g:> = dom g
by A1, Th50;
for x being object st x in dom g holds
g . x = h . x
hence
g = h
by A2, A3, A5, Th50; verum