let X be set ; :: thesis: for b, s being bag of X
for x being object holds support (Subst (b,x,s)) = ((support b) \ {x}) \/ (support s)
let b, s be bag of X; :: thesis: for x being object holds support (Subst (b,x,s)) = ((support b) \ {x}) \/ (support s)
let x be object ; :: thesis: support (Subst (b,x,s)) = ((support b) \ {x}) \/ (support s)
support (Subst (b,x,s)) = (support (b +* (x,0))) \/ (support s) by PRE_POLY:38;
hence support (Subst (b,x,s)) = ((support b) \ {x}) \/ (support s) by Th16; :: thesis: verum