take UNITSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_scalar n) #) ; :: thesis: ( 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 ) ; :: thesis: verum