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 & dom <:k,h:> = dom k ) by A1, A2, Th70;
for x being set st x in dom f holds
f . x = k . x

proof

let x be set ; :: 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, Def8;
hence f . x = k . x by A3, ZFMISC_1:33; :: thesis: verum

end;

hence f = k by A3, A4, FUNCT_1:9; :: thesis: g = h
A5: ( dom <:f,g:> = dom g & dom <:k,h:> = dom h ) by A1, A2, Th70;
for x being set st x in dom g holds
g . x = h . x

proof

let x be set ; :: 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, Def8;
hence g . x = h . x by A3, ZFMISC_1:33; :: thesis: verum

end;

hence g = h by A3, A5, FUNCT_1:9; :: thesis: verum