let S, S9 be non void Signature; :: thesis: for f, g being Function st f,g form_morphism_between S,S9 holds
f,g form_a_replacement_in S
let f, g be Function; :: thesis: ( f,g form_morphism_between S,S9 implies f,g form_a_replacement_in S )
A1: dom (id the carrier of S) = the carrier of S ;
A2: dom (id the carrier' of S) = the carrier' of S ;
assume A3: f,g form_morphism_between S,S9 ; :: thesis: f,g form_a_replacement_in S
then dom g = the carrier' of S ;
then A4: (id the carrier' of S) +* g = g by A2, FUNCT_4:19;
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 A5: ((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) )
dom f = the carrier of S by A3;
then A6: (id the carrier of S) +* f = f by A1, FUNCT_4:19;
hence ((id the carrier of S) +* f) * (the_arity_of o1) = the Arity of S9 . (g . o1) by A3
.= ((id the carrier of S) +* f) * (the_arity_of o2) by A3, A6, A4, A5 ;
:: thesis: ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2)
reconsider g9 = g as Function of the carrier' of S, the carrier' of S9 by A3, INSTALG1:9;
thus ((id the carrier of S) +* f) . (the_result_sort_of o1) = (f * the ResultSort of S) . o1 by A6, FUNCT_2:15
.= ( the ResultSort of S9 * g) . o1 by A3
.= the ResultSort of S9 . (g9 . o1) by FUNCT_2:15
.= ( the ResultSort of S9 * g9) . o2 by A4, A5, FUNCT_2:15
.= (f * the ResultSort of S) . o2 by A3
.= ((id the carrier of S) +* f) . (the_result_sort_of o2) by A6, FUNCT_2:15 ; :: thesis: verum