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