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

proof

let x be object ; :: 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

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

end;

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

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

end;

end;

end;

A7: dom q = X by PARTFUN1:def 2;
dom p = X by PARTFUN1:def 2;
hence p = q by A4, A7, FUNCT_1:2; :: thesis: verum