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

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

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

( dom (s +* g) = (dom s) \/ (dom g) & dom s = dom f )
by CARD_3:9, FUNCT_4:def 1;(s +* g) . x in f . x

let x be object ; :: thesis: ( x in dom f implies (s +* g) . b_{1} in f . b_{1} )

assume A4: x in dom f ; :: thesis: (s +* g) . b_{1} in f . b_{1}

end;assume A4: x in dom f ; :: thesis: (s +* g) . b

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

end;

suppose A6:
not x in dom g
; :: thesis: (s +* g) . b_{1} in f . b_{1}

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;( 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

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