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

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