let S be non void Signature; :: thesis: for f, g 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 f, g 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 ;
A5: (id the carrier' of S) . o2 = o2 ;
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: g . o1 in rng g by FUNCT_1:def 3;
A8: ((id the carrier' of S) +* g) . o1 = g . o1 by A6, FUNCT_4:13;
then ( not o2 in dom g implies g . o1 = o2 ) by A3, A5, FUNCT_4:11;
then A9: ( 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:13;
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, A8, A9; :: thesis: verum
end;
suppose A10: 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 A11: not o1 in the carrier' of S /\ (rng g) by A2;
A12: ((id the carrier' of S) +* g) . o1 = o1 by A4, A10, FUNCT_4:11;
then ( o2 in dom g implies ( o1 = g . o2 & g . o2 in rng g ) ) by A3, FUNCT_1:def 3, FUNCT_4:13;
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, A12, A11, FUNCT_4:11, XBOOLE_0:def 4; :: thesis: verum
end;
end;