let f, g be non-empty Function; :: thesis: ( product f c= product g implies ( dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) ) )
assume A1: product f c= product g ; :: thesis: ( dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) )
consider h being Element of product f;
h in product f ;
then 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;
hence dom f = dom g ; :: thesis: for x being set st x in dom f holds
f . x c= g . x
let x be set ; :: thesis: ( x in dom f implies f . x c= g . x )
assume A3: x in dom f ; :: thesis: f . x c= g . x
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in f . x or z in g . x )
consider k being Element of product f;
reconsider k = k as Function ;
defpred S₁[ set ] means $1 = x;
deffunc H₁( set ) -> set = z;
deffunc H₂( set ) -> set = k . $1;
consider h being Function such that
A4: ( dom h = dom f & ( for y being set st y in dom f holds
( ( S₁[y] implies h . y = H₁(y) ) & ( not S₁[y] implies h . y = H₂(y) ) ) ) ) from PARTFUN1:sch 1();
assume A5: z in f . x ; :: thesis: z in g . x

now

let y be set ; :: thesis: ( y in dom f implies h . y in f . y )
assume y in dom f ; :: thesis: h . y in f . y
then ( ( y = x implies h . y = z ) & ( y <> x implies h . y = k . y ) & k . y in f . y ) by A4, CARD_3:18;
hence h . y in f . y by A5; :: thesis: verum

end;

then h in product f by A4, CARD_3:18;
then h . x in g . x by A1, A2, A3, CARD_3:18;
hence z in g . x by A3, A4; :: thesis: verum