let A be non empty partial non-empty UAStr ; :: thesis: ( A is ECIW-strict implies for o being OperSymbol of A holds
( o = 1 or o = 2 or o = 3 or o = 4 ) )
assume signature A = ECIW-signature ; :: according to AOFA_000:def 27 :: thesis: for o being OperSymbol of A holds
( o = 1 or o = 2 or o = 3 or o = 4 )
then 4 = len the charact of A by Th54, UNIALG_1:def 4;
then dom the charact of A = Seg 4 by FINSEQ_1:def 3;
hence for o being OperSymbol of A holds
( o = 1 or o = 2 or o = 3 or o = 4 ) by ENUMSET1:def 2, FINSEQ_3:2; :: thesis: verum