let I be set ; :: thesis: for f being V2() 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 V2() 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) . b1 in f . b1 )
assume A4: x in dom f ; :: thesis: (s +* g) . b1 in f . b1
per cases ( x in dom g or not x in dom g ) ;
suppose A5: x in dom g ; :: thesis: (s +* g) . b1 in f . b1
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) . b1 in f . b1
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 ;
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 ;
then dom (s +* g) = dom f by ;
hence s +* g is Element of product f by ; :: thesis: verum