let S be non void Signature; :: thesis: for f being Function holds f, {} form_a_replacement_in S
let f be Function; :: thesis: f, {} form_a_replacement_in S
reconsider g = {} as Function ;
f,g form_a_replacement_in S

proof

let o1, o2 be OperSymbol of S; :: according to ALGSPEC1:def 3 :: thesis: ( ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 implies ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) )
A1: (id the carrier' of S) +* g = id the carrier' of S by FUNCT_4:22;
assume ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 ; :: thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
then o1 = (id the carrier' of S) . o2 by A1, FUNCT_1:34
.= o2 by FUNCT_1:34 ;
hence ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) ; :: thesis: verum

end;

hence f, {} form_a_replacement_in S ; :: thesis: verum