let p be Element of GRZ-ops ; :: thesis: ( dom p = Seg 1 & p . 1 <> 0 )
A1: ( p = 'not' implies ( dom p = Seg 1 & p . 1 <> 0 ) ) by FINSEQ_1:def 8;
A2: ( p = '&' implies ( dom p = Seg 1 & p . 1 <> 0 ) ) by FINSEQ_1:def 8;
( p = '=' implies ( dom p = Seg 1 & p . 1 <> 0 ) ) by FINSEQ_1:def 8;
hence ( dom p = Seg 1 & p . 1 <> 0 ) by A1, A2, ENUMSET1:def 1; :: thesis: verum