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 Th7;
hence ~ o is Function of [: the carrier of (opp V), the carrier of (opp K):], the carrier of (opp V) ; :: thesis: verum