let I be set ; :: thesis: for f being non-empty ManySortedSet of I
for g being Function
for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
let f be non-empty ManySortedSet of I; :: thesis: for g being Function
for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
let g be Function; :: thesis: for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) holds
s +* g is Element of product f
let s be Element of product f; :: thesis: ( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) implies s +* g is Element of product f )
assume that
A1: dom g c= dom f and
A2: for x being set st x in dom g holds
g . x in f . x ; :: thesis: s +* g is Element of product f

A3: now :: thesis: for x being object st x in dom f holds
(s +* g) . x in f . x

let x be object ; :: thesis: ( x in dom f implies (s +* g) . b₁ in f . b₁ )
assume A4: x in dom f ; :: thesis: (s +* g) . b₁ in f . b₁

per cases ( x in dom g or not x in dom g ) ;

suppose A5: x in dom g ; :: thesis: (s +* g) . b₁ in f . b₁

then (s +* g) . x = g . x by FUNCT_4:13;
hence (s +* g) . x in f . x by A2, A5; :: thesis: verum

end;

suppose A6: not x in dom g ; :: thesis: (s +* g) . b₁ in f . b₁

A7: ex g9 being Function st
( s = g9 & dom g9 = dom f & ( for x being object st x in dom f holds
g9 . x in f . x ) ) by CARD_3:def 5;
(s +* g) . x = s . x by A6, FUNCT_4:11;
hence (s +* g) . x in f . x by A4, A7; :: thesis: verum

end;

end;

end;

( dom (s +* g) = (dom s) \/ (dom g) & dom s = dom f ) by CARD_3:9, FUNCT_4:def 1;
then dom (s +* g) = dom f by A1, XBOOLE_1:12;
hence s +* g is Element of product f by A3, CARD_3:9; :: thesis: verum