let G be non empty addLoopStr ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( w is associating implies p @ p = p )
A1: w . (p,p) = w . (p,p) ;
assume w is associating ; :: thesis: p @ p = p
hence p @ p = p by A1; :: thesis: verum