let f1, f2 be Element of Funcs (Valuations_in A),BOOLEAN ; :: thesis: ( ( for v being Element of Valuations_in A holds f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } ) & ( for v being Element of Valuations_in A holds f2 . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } ) implies f1 = f2 )
assume that
A2: for v being Element of Valuations_in A holds f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } and
A3: for v being Element of Valuations_in A holds f2 . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } ; :: thesis: f1 = f2
for v being Element of Valuations_in A holds f1 . v = f2 . v

proof

let v be Element of Valuations_in A; :: thesis: f1 . v = f2 . v
f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } by A2;
hence f1 . v = f2 . v by A3; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:113; :: thesis: verum