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) ) ) )

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

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 that 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;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

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