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 M,G are_associated_wrp w 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 M,G are_associated_wrp w 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 M,G are_associated_wrp w holds
p @ p = p
let w be Function of [: the carrier of M, the carrier of M:], the carrier of G; :: thesis: ( M,G are_associated_wrp w implies p @ p = p )
A1: w . (p,p) = w . (p,p) ;
assume M,G are_associated_wrp w ; :: thesis: p @ p = p
hence p @ p = p by A1, Def2; :: thesis: verum