let f1, f2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); :: thesis: ( ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f1 . v = TRUE ) & ( f1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f1 . v = FALSE ) & ( f1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f2 . v = TRUE ) & ( f2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f2 . v = FALSE ) & ( f2 . v = FALSE implies not v *' ll in r ) ) ) implies f1 = f2 )
assume that
A3: for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f1 . v = TRUE ) & ( f1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f1 . v = FALSE ) & ( f1 . v = FALSE implies not v *' ll in r ) ) and
A4: for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f2 . v = TRUE ) & ( f2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f2 . v = FALSE ) & ( f2 . v = FALSE implies not v *' ll in r ) ) ; :: 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
per cases ( v *' ll in r or not v *' ll in r ) ;
suppose A5: v *' ll in r ; :: thesis: f1 . v = f2 . v
then f1 . v = TRUE by A3;
hence f1 . v = f2 . v by A4, A5; :: thesis: verum
end;
suppose A6: not v *' ll in r ; :: thesis: f1 . v = f2 . v
then f1 . v = FALSE by A3;
hence f1 . v = f2 . v by A4, A6; :: thesis: verum
end;
end;
end;
hence f1 = f2 by FUNCT_2:63; :: thesis: verum