let X be set ; :: thesis: for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)
let b1, b2, b3 be real-valued ManySortedSet of X; :: thesis: (b1 + b2) + b3 = b1 + (b2 + b3)
now :: thesis: for x being object st x in X holds
((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x
let x be object ; :: thesis: ( x in X implies ((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x )
assume x in X ; :: thesis: ((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x
thus ((b1 + b2) + b3) . x = ((b1 + b2) . x) + (b3 . x) by Def5
.= ((b1 . x) + (b2 . x)) + (b3 . x) by Def5
.= (b1 . x) + ((b2 . x) + (b3 . x))
.= (b1 . x) + ((b2 + b3) . x) by Def5
.= (b1 + (b2 + b3)) . x by Def5 ; :: thesis: verum
end;
hence (b1 + b2) + b3 = b1 + (b2 + b3) ; :: thesis: verum