let S, S' be non void Signature; :: thesis: for f, g being Function st f,g form_morphism_between S,S' holds
f,g form_a_replacement_in S
let f, g be Function; :: thesis: ( f,g form_morphism_between S,S' implies f,g form_a_replacement_in S )
assume A1: f,g form_morphism_between S,S' ; :: thesis: f,g form_a_replacement_in S
then ( dom f = the carrier of S & dom (id the carrier of S) = the carrier of S ) by PUA2MSS1:def 13, RELAT_1:71;
then A2: (id the carrier of S) +* f = f by FUNCT_4:20;
( dom g = the carrier' of S & dom (id the carrier' of S) = the carrier' of S ) by A1, PUA2MSS1:def 13, RELAT_1:71;
then A3: (id the carrier' of S) +* g = g by FUNCT_4:20;
reconsider g' = g as Function of the carrier' of S,the carrier' of S' by A1, INSTALG1:10;
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 A4: ((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) )
thus ((id the carrier of S) +* f) * (the_arity_of o1) = the Arity of S' . (g . o1) by A1, A2, PUA2MSS1:def 13
.= ((id the carrier of S) +* f) * (the_arity_of o2) by A1, A2, A3, A4, PUA2MSS1:def 13 ; :: thesis: ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2)
thus ((id the carrier of S) +* f) . (the_result_sort_of o1) = (f * the ResultSort of S) . o1 by A2, FUNCT_2:21
.= (the ResultSort of S' * g) . o1 by A1, PUA2MSS1:def 13
.= the ResultSort of S' . (g' . o1) by FUNCT_2:21
.= (the ResultSort of S' * g') . o2 by A3, A4, FUNCT_2:21
.= (f * the ResultSort of S) . o2 by A1, PUA2MSS1:def 13
.= ((id the carrier of S) +* f) . (the_result_sort_of o2) by A2, FUNCT_2:21 ; :: thesis: verum