defpred S₁[ object , object ] means ( ( $1 = 'not' & $2 = 1 ) or ( ( $1 = '&' or $1 = '=' ) & $2 = 2 ) );
A10: for a being object st a in GRZ-ops holds
ex b being object st
( b in NAT & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in GRZ-ops implies ex b being object st
( b in NAT & S₁[a,b] ) )
assume a in GRZ-ops ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )
then ( a = 'not' or a = '&' or a = '=' ) by ENUMSET1:def 1;
hence ex b being object st
( b in NAT & S₁[a,b] ) ; :: thesis: verum

end;

consider f being Function of GRZ-ops,NAT such that
A21: for a being object st a in GRZ-ops holds
S₁[a,f . a] from FUNCT_2:sch 1(A10);
take f ; :: thesis: ( f . 'not' = 1 & f . '&' = 2 & f . '=' = 2 )
( 'not' in GRZ-ops & '&' in GRZ-ops & '=' in GRZ-ops ) by ENUMSET1:def 1;
hence ( f . 'not' = 1 & f . '&' = 2 & f . '=' = 2 ) by A21, Th1; :: thesis: verum