let M be Function; :: thesis: ( M = f .. x iff ( dom M = I & ( 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: ( dom M = I & ( 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: ( dom M = I & ( 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;
hence dom M = I by PARTFUN1:def 4; :: thesis: for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i)
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 that
A3: dom M = I and
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
A4: dom f = I by PARTFUN1:def 4;
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