let S be non void Signature; :: thesis: for g, f being Function st g is one-to-one & the carrier' of S /\ (rng g) c= dom g holds
f,g form_a_replacement_in S
let g, f be Function; :: thesis: ( g is one-to-one & the carrier' of S /\ (rng g) c= dom g implies f,g form_a_replacement_in S )
assume that
A1: g is one-to-one and
A2: the carrier' of S /\ (rng g) c= dom g ; :: thesis: f,g form_a_replacement_in S
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) ) )
assume A3: ((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) )
A4: (id the carrier' of S) . o1 = o1 by FUNCT_1:35;
A5: (id the carrier' of S) . o2 = o2 by FUNCT_1:35;

per cases ( o1 in dom g or not o1 in dom g ) ;

suppose A6: o1 in dom g ; :: 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 A7: ( ((id the carrier' of S) +* g) . o1 = g . o1 & g . o1 in rng g ) by FUNCT_1:def 5, FUNCT_4:14;
then ( not o2 in dom g implies g . o1 = o2 ) by A3, A5, FUNCT_4:12;
then A8: ( not o2 in dom g implies o2 in the carrier' of S /\ (rng g) ) by A7, XBOOLE_0:def 4;
then ((id the carrier' of S) +* g) . o2 = g . o2 by A2, FUNCT_4:14;
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) ) by A1, A2, A3, A6, A7, A8, FUNCT_1:def 8; :: thesis: verum

end;

suppose not o1 in dom g ; :: 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 A9: ( ((id the carrier' of S) +* g) . o1 = o1 & not o1 in the carrier' of S /\ (rng g) ) by A2, A4, FUNCT_4:12;
then ( o2 in dom g implies ( o1 = g . o2 & g . o2 in rng g ) ) by A3, FUNCT_1:def 5, FUNCT_4:14;
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) ) by A3, A5, A9, FUNCT_4:12, XBOOLE_0:def 4; :: thesis: verum

end;

end;