let X be set ; :: thesis: for p, q being ManySortedSet of st p | (support p) = q | (support q) holds
p = q
let p, q be ManySortedSet of ; :: thesis: ( p | (support p) = q | (support q) implies p = q )
assume A1: p | (support p) = q | (support q) ; :: thesis: p = q
A2: dom (p | (support p)) = (dom p) /\ (support p) by RELAT_1:90
.= support p by POLYNOM1:41, XBOOLE_1:28 ;
A3: dom (q | (support q)) = (dom q) /\ (support q) by RELAT_1:90
.= support q by POLYNOM1:41, XBOOLE_1:28 ;
A4: for x being set st x in X holds
p . x = q . x

proof

let x be set ; :: thesis: ( x in X implies p . x = q . x )
assume x in X ; :: thesis: p . x = q . x

per cases ( x in support p or not x in support p ) ;

suppose A5: x in support p ; :: thesis: p . x = q . x

thus p . x = (p | (support p)) . x by A5, FUNCT_1:72
.= q . x by A1, A2, A3, A5, FUNCT_1:72 ; :: thesis: verum

end;

suppose A6: not x in support p ; :: thesis: p . x = q . x

thus p . x = 0 by A6, POLYNOM1:def 7
.= q . x by A1, A2, A3, A6, POLYNOM1:def 7 ; :: thesis: verum

end;

end;

end;

( dom p = X & dom q = X ) by PARTFUN1:def 4;
hence p = q by A4, FUNCT_1:9; :: thesis: verum