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

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

hence
J = {i} --> (J . i)
by A1, FUNCT_1:2; :: thesis: verum
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;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