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

proof

assume A4: f = b1 + b2 ; :: thesis: for x being set holds f . x = (b1 . x) + (b2 . x)
let x be set ; :: 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 A2, A3, A4, VALUED_1:def 1; :: thesis: verum

end;

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

then ( b1 . x = 0 & b2 . x = 0 ) by A2, FUNCT_1:def 4;
hence f . x = (b1 . x) + (b2 . x) by A2, A3, A5, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

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