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