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