take
UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #)
; ( the carrier of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = REAL n & 0. UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = 0* n & the addF of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_add n & the Mult of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_mult n & the scalar of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_scalar n )
thus
( the carrier of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = REAL n & 0. UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = 0* n & the addF of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_add n & the Mult of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_mult n & the scalar of UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) = Euclid_scalar n )
; verum