defpred S₁[ object , object ] means ( ( $1 in GRZ-ops implies $2 = GRZ-op-arity . $1 ) & ( not $1 in GRZ-ops implies $2 = 0 ) );
A1: for a being object st a in GRZ-symbols holds
ex b being object st
( b in NAT & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in GRZ-symbols implies ex b being object st
( b in NAT & S₁[a,b] ) )
assume a in GRZ-symbols ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )

per cases ( not a in GRZ-ops or a in GRZ-ops ) ;

suppose not a in GRZ-ops ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )

hence ex b being object st
( b in NAT & S₁[a,b] ) ; :: thesis: verum

end;

suppose A5: a in GRZ-ops ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )

take GRZ-op-arity . a ; :: thesis: ( GRZ-op-arity . a in NAT & S₁[a,GRZ-op-arity . a] )
thus ( GRZ-op-arity . a in NAT & S₁[a,GRZ-op-arity . a] ) by A5, FUNCT_2:5; :: thesis: verum

end;

end;

end;

consider f being Function of GRZ-symbols,NAT such that
A10: for a being object st a in GRZ-symbols holds
S₁[a,f . a] from FUNCT_2:sch 1(A1);
set p = the Element of VAR ;
A11: the Element of VAR in GRZ-symbols by XBOOLE_0:def 3;
not the Element of VAR in GRZ-ops by Lm4;
then f . the Element of VAR = 0 by A10, A11;
then reconsider f = f as Polish-arity-function of GRZ-symbols by A11, POLNOT_1:def 18;
take f ; :: thesis: for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies f . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f . a = 0 ) )
let a be object ; :: thesis: ( a in GRZ-symbols implies ( ( a in GRZ-ops implies f . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f . a = 0 ) ) )
assume a in GRZ-symbols ; :: thesis: ( ( a in GRZ-ops implies f . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f . a = 0 ) )
hence ( ( a in GRZ-ops implies f . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f . a = 0 ) ) by A10; :: thesis: verum