let f1, f2 be Polish-arity-function of GRZ-symbols ; :: thesis: ( ( for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies f1 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f1 . a = 0 ) ) ) & ( for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies f2 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f2 . a = 0 ) ) ) implies f1 = f2 )
assume that
A1: for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies f1 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f1 . a = 0 ) ) and
A2: for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies f2 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies f2 . a = 0 ) ) ; :: thesis: f1 = f2
dom f1 = GRZ-symbols by FUNCT_2:def 1;
then A3: dom f1 = dom f2 by FUNCT_2:def 1;
for a being object st a in dom f1 holds
f1 . a = f2 . a
proof
let a be object ; :: thesis: ( a in dom f1 implies f1 . a = f2 . a )
assume A4: a in dom f1 ; :: thesis: f1 . a = f2 . a
per cases ( a in GRZ-ops or not a in GRZ-ops ) ;
suppose A5: a in GRZ-ops ; :: thesis: f1 . a = f2 . a
hence f1 . a = GRZ-op-arity . a by A1, A4
.= f2 . a by A2, A4, A5 ;
:: thesis: verum
end;
suppose A6: not a in GRZ-ops ; :: thesis: f1 . a = f2 . a
hence f1 . a = 0 by A1, A4
.= f2 . a by A2, A4, A6 ;
:: thesis: verum
end;
end;
end;
hence f1 = f2 by A3, FUNCT_1:2; :: thesis: verum