let X be set ; :: thesis: for b, b1, b2 being real-valued ManySortedSet of X st ( for x being object st x in X holds
b . x = (b1 . x) + (b2 . x) ) holds
b = b1 + b2
let b, b1, b2 be real-valued ManySortedSet of X; :: thesis: ( ( for x being object st x in X holds
b . x = (b1 . x) + (b2 . x) ) implies b = b1 + b2 )
assume A1: for x being object st x in X holds
b . x = (b1 . x) + (b2 . x) ; :: thesis: b = b1 + b2

now :: thesis: for x being object holds b . x = (b1 . x) + (b2 . x)

let x be object ; :: thesis: b . b₁ = (b1 . b₁) + (b2 . b₁)

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: b . b₁ = (b1 . b₁) + (b2 . b₁)

hence b . x = (b1 . x) + (b2 . x) by A1; :: thesis: verum

end;

suppose A2: not x in X ; :: thesis: b . b₁ = (b1 . b₁) + (b2 . b₁)

A3: dom b2 = X by PARTFUN1:def 2;
A4: dom b1 = X by PARTFUN1:def 2;
dom b = X by PARTFUN1:def 2;
hence b . x = 0 + 0 by A2, FUNCT_1:def 2
.= 0 + (b2 . x) by A2, A3, FUNCT_1:def 2
.= (b1 . x) + (b2 . x) by A2, A4, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;

end;

hence b = b1 + b2 by Def5; :: thesis: verum