let x be object ; :: thesis: for X being set
for p being ManySortedSet of X st support p = {x} holds
p = (X --> 0) +* (x,(p . x))
let X be set ; :: thesis: for p being ManySortedSet of X st support p = {x} holds
p = (X --> 0) +* (x,(p . x))
let p be ManySortedSet of X; :: thesis: ( support p = {x} implies p = (X --> 0) +* (x,(p . x)) )
assume A1: support p = {x} ; :: thesis: p = (X --> 0) +* (x,(p . x))
A2: for y being object st y in dom p holds
p . y = ((X --> 0) +* (x,(p . x))) . y

proof

let y be object ; :: thesis: ( y in dom p implies p . y = ((X --> 0) +* (x,(p . x))) . y )
assume y in dom p ; :: thesis: p . y = ((X --> 0) +* (x,(p . x))) . y
then y in X ;
then A3: y in dom (X --> 0) by FUNCOP_1:13;

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: p . y = ((X --> 0) +* (x,(p . x))) . y

hence p . y = ((X --> 0) +* (x,(p . x))) . y by A3, FUNCT_7:31; :: thesis: verum

end;

suppose A4: x <> y ; :: thesis: p . y = ((X --> 0) +* (x,(p . x))) . y

then not y in support p by A1, TARSKI:def 1;
then p . y = 0 by PRE_POLY:def 7;
hence p . y = ((X --> 0) +* (x,(p . x))) . y by A4, Lm1; :: thesis: verum

end;

end;

end;

dom ((X --> 0) +* (x,(p . x))) = dom (X --> 0) by FUNCT_7:30
.= X by FUNCOP_1:13 ;
then dom p = dom ((X --> 0) +* (x,(p . x))) by PARTFUN1:def 2;
hence p = (X --> 0) +* (x,(p . x)) by A2, FUNCT_1:2; :: thesis: verum