let f be ManySortedSet of X; :: thesis: ( f = b1 + b2 iff for x being object holds f . x = (b1 . x) + (b2 . x) )
A1: ( dom b1 = X & dom b2 = X ) by PARTFUN1:def 2;
then A2: dom f = (dom b1) /\ (dom b2) by PARTFUN1:def 2;
thus ( f = b1 + b2 implies for x being object holds f . x = (b1 . x) + (b2 . x) ) :: thesis: ( ( for x being object holds f . x = (b1 . x) + (b2 . x) ) implies f = b1 + b2 )

proof

assume A3: f = b1 + b2 ; :: thesis: for x being object holds f . x = (b1 . x) + (b2 . x)
let x be object ; :: thesis: f . x = (b1 . x) + (b2 . x)

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

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

hence f . x = (b1 . x) + (b2 . x) by A1, A2, A3, VALUED_1:def 1; :: thesis: verum

end;

suppose A4: not x in X ; :: thesis: f . x = (b1 . x) + (b2 . x)

then ( b1 . x = 0 & b2 . x = 0 ) by A1, FUNCT_1:def 2;
hence f . x = (b1 . x) + (b2 . x) by A1, A2, A4, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

assume for x being object holds f . x = (b1 . x) + (b2 . x) ; :: thesis: f = b1 + b2
then for c being object st c in dom f holds
f . c = (b1 . c) + (b2 . c) ;
hence f = b1 + b2 by A2, VALUED_1:def 1; :: thesis: verum