let f, g be non-empty Function; :: thesis: ( product f = product g implies f = g )
assume A1: product f = product g ; :: thesis: f = g
consider h being Element of product f;
A2: ( ex i being Function st
( h = i & dom i = dom g & ( for x being set st x in dom g holds
i . x in g . x ) ) & ex i being Function st
( h = i & dom i = dom f & ( for x being set st x in dom f holds
i . x in f . x ) ) ) by A1, CARD_3:def 5;

now

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then ( f . x c= g . x & g . x c= f . x ) by A1, A2, Th1;
hence f . x = g . x by XBOOLE_0:def 10; :: thesis: verum

end;

hence f = g by A2, FUNCT_1:9; :: thesis: verum