let i be object ; :: thesis: for J being ManySortedSet of {i} holds J = {i} --> (J . i)
let J be ManySortedSet of {i}; :: thesis: J = {i} --> (J . i)
A1: dom J = {i} by PARTFUN1:def 2
.= dom ({i} --> (J . i)) ;
for x being object st x in dom J holds
J . x = ({i} --> (J . i)) . x
proof
let x be object ; :: thesis: ( x in dom J implies J . x = ({i} --> (J . i)) . x )
assume x in dom J ; :: thesis: J . x = ({i} --> (J . i)) . x
then A2: x = i by TARSKI:def 1;
({i} --> (J . i)) . i = (i .--> (J . i)) . i by FUNCOP_1:def 9
.= J . i by FUNCOP_1:72 ;
hence J . x = ({i} --> (J . i)) . x by A2; :: thesis: verum
end;
hence J = {i} --> (J . i) by A1, FUNCT_1:2; :: thesis: verum