let G be non empty addLoopStr ; for M being non empty MidStr
for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
let M be non empty MidStr ; for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
let p be Point of M; for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; ( w is associating implies p @ p = p )
A1:
w . (p,p) = w . (p,p)
;
assume
w is associating
; p @ p = p
hence
p @ p = p
by A1; verum