let S, S9 be non void Signature; 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; ( 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
; 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; ALGSPEC1:def 3 ( ((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
; ( ((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
;
((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
; verum