let f, g be Function; :: thesis: ( dom f = dom g & ( for x being object st x in dom f holds
f . x c= g . x ) implies product f c= product g )
assume that
A1: dom f = dom g and
A2: for x being object st x in dom f holds
f . x c= g . x ; :: thesis: product f c= product g
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product f or x in product g )
assume x in product f ; :: thesis: x in product g
then consider f1 being Function such that
A3: x = f1 and
A4: dom f1 = dom f and
A5: for x being object st x in dom f holds
f1 . x in f . x by Def5;

now :: thesis: for x being object st x in dom g holds
f1 . x in g . x

let x be object ; :: thesis: ( x in dom g implies f1 . x in g . x )
assume A6: x in dom g ; :: thesis: f1 . x in g . x
then A7: f1 . x in f . x by A1, A5;
f . x c= g . x by A1, A2, A6;
hence f1 . x in g . x by A7; :: thesis: verum

end;

hence x in product g by A1, A3, A4, Def5; :: thesis: verum