let f, g be Function of GRZ-ops,NAT; :: thesis: ( f . 'not' = 1 & f . '&' = 2 & f . '=' = 2 & g . 'not' = 1 & g . '&' = 2 & g . '=' = 2 implies f = g )
assume that
A1: ( f . 'not' = 1 & f . '&' = 2 & f . '=' = 2 ) and
A2: ( g . 'not' = 1 & g . '&' = 2 & g . '=' = 2 ) ; :: thesis: f = g
dom f = GRZ-ops by FUNCT_2:def 1;
then A11: dom f = dom g by FUNCT_2:def 1;
for a being object st a in dom f holds
f . a = g . a
proof
let a be object ; :: thesis: ( a in dom f implies f . a = g . a )
assume a in dom f ; :: thesis: f . a = g . a
then ( a = 'not' or a = '&' or a = '=' ) by ENUMSET1:def 1;
hence f . a = g . a by A1, A2; :: thesis: verum
end;
hence f = g by A11, FUNCT_1:2; :: thesis: verum