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, B being MSAlgebra of S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | S1,f,g),(B | S1,f,g) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A <> {} & Args o2,B <> {} holds
for x2 being Element of Args o2,A
for x1 being Element of Args o1,(A | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for A, B being MSAlgebra of S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | S1,f,g),(B | S1,f,g) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A <> {} & Args o2,B <> {} holds
for x2 being Element of Args o2,A
for x1 being Element of Args o1,(A | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for A, B being MSAlgebra of S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | S1,f,g),(B | S1,f,g) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A <> {} & Args o2,B <> {} holds
for x2 being Element of Args o2,A
for x1 being Element of Args o1,(A | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let A2, B2 be MSAlgebra of S2; :: thesis: for h2 being ManySortedFunction of A2,B2
for h1 being ManySortedFunction of (A2 | S1,f,g),(B2 | S1,f,g) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A2 <> {} & Args o2,B2 <> {} holds
for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
set A1 = A2 | S1,f,g;
set B1 = B2 | S1,f,g;
let h2 be ManySortedFunction of A2,B2; :: thesis: for h1 being ManySortedFunction of (A2 | S1,f,g),(B2 | S1,f,g) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A2 <> {} & Args o2,B2 <> {} holds
for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let h1 be ManySortedFunction of (A2 | S1,f,g),(B2 | S1,f,g); :: thesis: ( h1 = h2 * f implies for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A2 <> {} & Args o2,B2 <> {} holds
for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A2: h1 = h2 * f ; :: thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A2 <> {} & Args o2,B2 <> {} holds
for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let o1 be OperSymbol of S1; :: thesis: for o2 being OperSymbol of S2 st o2 = g . o1 & Args o2,A2 <> {} & Args o2,B2 <> {} holds
for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let o2 be OperSymbol of S2; :: thesis: ( o2 = g . o1 & Args o2,A2 <> {} & Args o2,B2 <> {} implies for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A3: o2 = g . o1 ; :: thesis: ( not Args o2,A2 <> {} or not Args o2,B2 <> {} or for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A4: ( Args o2,A2 <> {} & Args o2,B2 <> {} ) ; :: thesis: for x2 being Element of Args o2,A2
for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let x2 be Element of Args o2,A2; :: thesis: for x1 being Element of Args o1,(A2 | S1,f,g) st x2 = x1 holds
h1 # x1 = h2 # x2
let x1 be Element of Args o1,(A2 | S1,f,g); :: thesis: ( x2 = x1 implies h1 # x1 = h2 # x2 )
assume A5: x2 = x1 ; :: thesis: h1 # x1 = h2 # x2
then reconsider f1 = x1, f2 = x2, g2 = h2 # x2 as Function by A4, MSUALG_6:1;
A6: ( Args o2,A2 = Args o1,(A2 | S1,f,g) & Args o2,B2 = Args o1,(B2 | S1,f,g) ) by A1, A3, Th25;
then A7: ( dom f1 = dom (the_arity_of o1) & dom f2 = dom (the_arity_of o2) ) by A4, MSUALG_3:6;

now

let i be natural number ; :: thesis: ( i in dom f1 implies g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) )
assume A8: i in dom f1 ; :: thesis: g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i)
dom f = the carrier of S1 by A1, PUA2MSS1:def 13;
then h1 . ((the_arity_of o1) /. i) = h2 . (f . ((the_arity_of o1) /. i)) by A2, FUNCT_1:23
.= h2 . (f . ((the_arity_of o1) . i)) by A7, A8, PARTFUN1:def 8
.= h2 . ((f * (the_arity_of o1)) . i) by A7, A8, FUNCT_1:23
.= h2 . ((the_arity_of o2) . i) by A1, A3, PUA2MSS1:def 13
.= h2 . ((the_arity_of o2) /. i) by A5, A7, A8, PARTFUN1:def 8 ;
hence g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) by A4, A5, A8, MSUALG_3:24; :: thesis: verum

end;

hence h1 # x1 = h2 # x2 by A4, A6, MSUALG_3:24; :: thesis: verum