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 Th12;
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