let f, g, h, k be Function; :: thesis: ( 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:> ; :: thesis: ( 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

proof

let x be object ; :: thesis: ( x in dom f implies f . x = k . x )
assume x in dom f ; :: thesis: f . x = k . x
then ( <:f,g:> . x = [(f . x),(g . x)] & <:k,h:> . x = [(k . x),(h . x)] ) by A3, A4, Def7;
hence f . x = k . x by A3, XTUPLE_0:1; :: thesis: verum

end;

hence f = k by A2, A3, A4, Th50; :: thesis: 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

proof

let x be object ; :: thesis: ( x in dom g implies g . x = h . x )
assume x in dom g ; :: thesis: g . x = h . x
then ( <:f,g:> . x = [(f . x),(g . x)] & <:k,h:> . x = [(k . x),(h . x)] ) by A3, A5, Def7;
hence g . x = h . x by A3, XTUPLE_0:1; :: thesis: verum

end;

hence g = h by A2, A3, A5, Th50; :: thesis: verum