let V be non empty RLSStruct ; :: thesis: for V1 being non empty add-closed multi-closed Subset of
for v, u being VECTOR of
for w1, w2 being VECTOR of st w1 = v & w2 = u holds
w1 + w2 = v + u
let V1 be non empty add-closed multi-closed Subset of ; :: thesis: for v, u being VECTOR of
for w1, w2 being VECTOR of st w1 = v & w2 = u holds
w1 + w2 = v + u
let v, u be VECTOR of ; :: thesis: for w1, w2 being VECTOR of st w1 = v & w2 = u holds
w1 + w2 = v + u
let w1, w2 be VECTOR of ; :: thesis: ( w1 = v & w2 = u implies w1 + w2 = v + u )
assume A1: ( w1 = v & w2 = u ) ; :: thesis: w1 + w2 = v + u
then [v,u] in [:V1,V1:] by ZFMISC_1:106;
hence w1 + w2 = v + u by A1, FUNCT_1:72; :: thesis: verum