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