let X be set ; :: thesis: for b, b1, b2 being natural-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 natural-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 . b1 = (b1 . b1) -' (b2 . b1)
per cases ( x in X or not x in X ) ;
suppose x in X ; :: thesis: b . b1 = (b1 . b1) -' (b2 . b1)
hence b . x = (b1 . x) -' (b2 . x) by A1; :: thesis: verum
end;
suppose A2: not x in X ; :: thesis: b . b1 = (b1 . b1) -' (b2 . b1)
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 by A2, FUNCT_1:def 2
.= 0 -' 0 by XREAL_1:232
.= 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 Def6; :: thesis: verum