addLoopStr(# the carrier of (opp V),the addF of (opp V),the ZeroF of (opp V) #) = addLoopStr(# the carrier of V,the addF of V,the ZeroF of V #) by Th9;
hence ~ o is Function of [:the carrier of (opp V),the carrier of (opp K):],the carrier of (opp V) ; :: thesis: verum