let S1, S2 be non empty non void ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )

let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) )

assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )

A2: dom f = the carrier of S1 by A1;
let A be MSAlgebra over S2; :: thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )

let o1 be OperSymbol of S1; :: thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )

let o2 be OperSymbol of S2; :: thesis: ( o2 = g . o1 implies ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) )
assume A3: o2 = g . o1 ; :: thesis: ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
thus Args (o2,A) = product ( the Sorts of A * ()) by PRALG_2:3
.= product ( the Sorts of A * (f * ())) by A1, A3
.= product (( the Sorts of A * f) * ()) by RELAT_1:36
.= product ( the Sorts of (A | (S1,f,g)) * ()) by
.= Args (o1,(A | (S1,f,g))) by PRALG_2:3 ; :: thesis: Result (o1,(A | (S1,f,g))) = Result (o2,A)
dom g = the carrier' of S1 by A1;
then the_result_sort_of o2 = ( the ResultSort of S2 * g) . o1 by
.= (f * the ResultSort of S1) . o1 by A1
.= f . () by FUNCT_2:15 ;
hence Result (o2,A) = the Sorts of A . (f . ()) by PRALG_2:3
.= ( the Sorts of A * f) . () by
.= the Sorts of (A | (S1,f,g)) . () by
.= Result (o1,(A | (S1,f,g))) by PRALG_2:3 ;
:: thesis: verum