:: deftheorem defines # CARDFIL4:def 7 :
for s being Function of [:NAT,NAT:],REAL holds # s = s;