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 A1: 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) ) )
hence A2: dom M = I by PARTFUN1:def 2; :: thesis: for i being set st i in I holds
for g being Function st g = f . i holds
M . i = g . (x . i)
thus 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, A2, Def17; :: thesis: verum

end;

assume that
A3: dom M = I and
A4: 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
A5: dom f = I by PARTFUN1:def 2;
then A6: for i being set st i in dom f holds
M . i = (f . i) . (x . i) by A4;
dom M = I /\ I by A3
.= I /\ (dom x) by PARTFUN1:def 2
.= (dom f) /\ (dom x) by PARTFUN1:def 2 ;
hence M = f .. x by A3, A5, A6, Def17; :: thesis: verum