let fg1, fg2 be Function; :: thesis: ( dom fg1 = [:(dom f),(dom g):] & ( for x, y being object st x in dom f & y in dom g holds
fg1 . (x,y) = [(f . x),(g . y)] ) & dom fg2 = [:(dom f),(dom g):] & ( for x, y being object st x in dom f & y in dom g holds
fg2 . (x,y) = [(f . x),(g . y)] ) implies fg1 = fg2 )
assume that
A1: dom fg1 = [:(dom f),(dom g):] and
A2: for x, y being object st x in dom f & y in dom g holds
fg1 . (x,y) = [(f . x),(g . y)] and
A3: dom fg2 = [:(dom f),(dom g):] and
A4: for x, y being object st x in dom f & y in dom g holds
fg2 . (x,y) = [(f . x),(g . y)] ; :: thesis: fg1 = fg2
for p being object st p in [:(dom f),(dom g):] holds
fg1 . p = fg2 . p

proof

let p be object ; :: thesis: ( p in [:(dom f),(dom g):] implies fg1 . p = fg2 . p )
assume p in [:(dom f),(dom g):] ; :: thesis: fg1 . p = fg2 . p
then consider x, y being object such that
A5: ( x in dom f & y in dom g ) and
A6: p = [x,y] by ZFMISC_1:def 2;
( fg1 . (x,y) = [(f . x),(g . y)] & fg2 . (x,y) = [(f . x),(g . y)] ) by A2, A4, A5;
hence fg1 . p = fg2 . p by A6; :: thesis: verum

end;

hence fg1 = fg2 by A1, A3; :: thesis: verum