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 over 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 over 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 over 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 over 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 that
A4: Args (o2,A2) <> {} and
A5: 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 A6: x2 = x1 ; :: thesis: h1 # x1 = h2 # x2
then reconsider f1 = x1, f2 = x2, g2 = h2 # x2 as Function by A4, A5, MSUALG_6:1;
A7: Args (o2,A2) = Args (o1,(A2 | (S1,f,g))) by A1, A3, Th24;
then A8: dom f1 = dom (the_arity_of o1) by A4, MSUALG_3:6;
A9: dom f2 = dom (the_arity_of o2) by A4, MSUALG_3:6;

A10: now :: thesis: for i being Nat st i in dom f1 holds
g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i)

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

end;

Args (o2,B2) = Args (o1,(B2 | (S1,f,g))) by A1, A3, Th24;
hence h1 # x1 = h2 # x2 by A4, A5, A7, A10, MSUALG_3:24; :: thesis: verum