addLoopStr(# the carrier of (opp W),the addF of (opp W),the U2 of (opp W) #) = addLoopStr(# the carrier of W,the addF of W,the U2 of W #) by Th12;
then reconsider o' = ~ o as Function of [:the carrier of (opp K),the carrier of (opp W):],the carrier of (opp W) ;
o' 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