let f1, f2 be Function of Omega,REAL; :: thesis: ( ( for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies f1 . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies f1 . w = 0 ) ) ) & ( for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies f2 . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies f2 . w = 0 ) ) ) implies f1 = f2 )
assume that
A2: for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies f1 . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies f1 . w = 0 ) ) and
A3: for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies f2 . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies f2 . w = 0 ) ) ; :: thesis: f1 = f2
for w being Element of Omega holds f1 . w = f2 . w

proof

let w be Element of Omega; :: thesis: f1 . w = f2 . w

per cases ( (RV - (Omega --> K)) . w >= 0 or not (RV - (Omega --> K)) . w >= 0 ) ;

suppose A0: (RV - (Omega --> K)) . w >= 0 ; :: thesis: f1 . w = f2 . w

then f1 . w = (RV - (Omega --> K)) . w by A2;
hence f1 . w = f2 . w by A0, A3; :: thesis: verum

end;

suppose A0: not (RV - (Omega --> K)) . w >= 0 ; :: thesis: f1 . w = f2 . w

then f1 . w = 0 by A2;
hence f1 . w = f2 . w by A0, A3; :: thesis: verum

end;

end;

end;

hence f1 = f2 ; :: thesis: verum