:: deftheorem defines U-linear COHSP_1:def 15 :
for f being Function holds
( f is U-linear iff ( f is U-stable & f is union-distributive ) );