addLoopStr(# the carrier of V,the addF of V,the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the ZeroF of (RealVS V) #) by Def22;
hence not RealVS V is empty ; :: thesis: verum