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 ) )
set h = the Element of product f;
the Element of product f in product f ;
then 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;
hence dom f = dom g by A2; :: 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 A4: x in dom f ; :: thesis: f . x c= g . x
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f . x or z in g . x )
reconsider zz = z as set by TARSKI:1;
set k = the Element of product f;
reconsider k = the Element of product f as Function ;
defpred S₁[ object ] means $1 = x;
deffunc H₁( object ) -> set = zz;
deffunc H₂( object ) -> set = k . $1;
consider h being Function such that
A5: ( dom h = dom f & ( for y being object 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 A6: z in f . x ; :: thesis: z in g . x

now :: thesis: for y being object st y in dom f holds
h . y in f . y

let y be object ; :: thesis: ( y in dom f implies h . y in f . y )
assume A7: y in dom f ; :: thesis: h . y in f . y
then ( y <> x implies h . y = k . y ) by A5;
hence h . y in f . y by A5, A6, A7, CARD_3:9; :: thesis: verum

end;

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