let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: ( 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) ) )
hereby :: thesis: ( ( 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) ) ) implies f,g form_a_replacement_in S )
assume A1: f,g form_a_replacement_in S ; :: thesis: 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 o1, o2 be OperSymbol of S; :: thesis: ( ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 implies ( ( 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) ) )
A2: rng (the_arity_of o1) c= the carrier of S ;
A3: rng (the_arity_of o2) c= the carrier of S ;
assume ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 ; :: thesis: ( ( 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) )
then A4: ((id the carrier' of S) +* g) . o1 = ( the carrier' of S -indexing g) . o2 by Th8
.= ((id the carrier' of S) +* g) . o2 by Th8 ;
then ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) by A1;
hence ( the carrier of S -indexing f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) by A2, Th21
.= ( the carrier of S -indexing f) * (the_arity_of o2) by A3, Th21 ;
:: thesis: ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2)
thus ( the carrier of S -indexing f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o1) by Th8
.= ((id the carrier of S) +* f) . (the_result_sort_of o2) by A1, A4
.= ( the carrier of S -indexing f) . (the_result_sort_of o2) by Th8 ; :: thesis: verum
end;
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) ) ; :: 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) ) )
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 ; :: 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 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 ;
:: 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) = ( 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 ; :: thesis: verum