let f1, f2 be Element of Funcs (Valuations_in A),BOOLEAN ; :: thesis: ( ( for v being Element of Valuations_in A holds
( ( v *' ll in r implies f1 . v = TRUE ) & ( not v *' ll in r implies f1 . v = FALSE ) ) ) & ( for v being Element of Valuations_in A holds
( ( v *' ll in r implies f2 . v = TRUE ) & ( not v *' ll in r implies f2 . v = FALSE ) ) ) implies f1 = f2 )
assume that
A3: for v being Element of Valuations_in A holds
( ( v *' ll in r implies f1 . v = TRUE ) & ( not v *' ll in r implies f1 . v = FALSE ) ) and
A4: for v being Element of Valuations_in A holds
( ( v *' ll in r implies f2 . v = TRUE ) & ( not v *' ll in r implies f2 . v = FALSE ) ) ; :: 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

per cases ( v *' ll in r or not v *' ll in r ) ;

suppose v *' ll in r ; :: thesis: f1 . v = f2 . v

then ( f1 . v = TRUE & f2 . v = TRUE ) by A3, A4;
hence f1 . v = f2 . v ; :: thesis: verum

end;

suppose not v *' ll in r ; :: thesis: f1 . v = f2 . v

then ( f1 . v = FALSE & f2 . v = FALSE ) by A3, A4;
hence f1 . v = f2 . v ; :: thesis: verum

end;

end;

end;

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