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