:: deftheorem defines Carrier FIELD_12:def 5 :
for f being Field-yielding sequence holds Carrier f = union { the carrier of (f . i) where i is Element of NAT : verum } ;