let M be ManySortedSet of I; :: thesis: ( M = f .. x iff for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) )

hereby :: thesis: ( ( for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) ) implies M = f .. x )

assume M = f .. x ; :: thesis: for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i)
then A1: ( dom M = dom f & ( for i being set st i in dom f holds
M . i = (f . i) . (x . i) ) ) by Def17;
dom M = I by PBOOLE:def 3;
hence for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) by A1; :: thesis: verum

end;

assume A2: for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i) ; :: thesis: M = f .. x
A3: dom M = I by PBOOLE:def 3;
A4: dom f = I by PBOOLE:def 3;
then for i being set st i in dom f holds
M . i = (f . i) . (x . i) by A2;
hence M = f .. x by A3, A4, Def17; :: thesis: verum