addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) = addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #)
by Th9;

then reconsider o9 = ~ o as Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ;

o9 is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ;

hence ~ o is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ; :: thesis: verum

then reconsider o9 = ~ o as Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ;

o9 is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ;

hence ~ o is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ; :: thesis: verum