take
NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #)
; ( the carrier of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = REAL n & 0. NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = 0* n & the addF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_add n & the Mult of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_mult n & the normF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_norm n )
thus
( the carrier of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = REAL n & 0. NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = 0* n & the addF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_add n & the Mult of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_mult n & the normF of NORMSTR(# (REAL n),(0* n),(Euclid_add n),(Euclid_mult n),(Euclid_norm n) #) = Euclid_norm n )
; verum