let S be non empty non void ManySortedSign ; for f, g being Function holds
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )
let f, g be Function; ( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )
assume A5:
for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) )
; f,g form_a_replacement_in S
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) ) )
A6:
rng (the_arity_of o1) c= the carrier of S
;
A7:
rng (the_arity_of o2) c= the carrier of S
;
assume
((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) )
then A8: ( the carrier' of S -indexing g) . o1 =
((id the carrier' of S) +* g) . o2
by Th8
.=
( the carrier' of S -indexing g) . o2
by Th8
;
then
( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2)
by A5;
hence ((id the carrier of S) +* f) * (the_arity_of o1) =
( the carrier of S -indexing f) * (the_arity_of o2)
by A6, Th21
.=
((id the carrier of S) +* f) * (the_arity_of o2)
by A7, Th21
;
((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) =
( the carrier of S -indexing f) . (the_result_sort_of o1)
by Th8
.=
( the carrier of S -indexing f) . (the_result_sort_of o2)
by A5, A8
.=
((id the carrier of S) +* f) . (the_result_sort_of o2)
by Th8
; verum