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 ;
A7: Args (o2,A2) = Args (o1,(A2 | (S1,f,g))) by A1, A3, Th24;
then A8: dom f1 = dom () by ;
A9: dom f2 = dom () by ;
A10: now :: thesis: for i being Nat st i in dom f1 holds
g2 . i = (h1 . (() /. i)) . (f1 . i)
let i be Nat; :: thesis: ( i in dom f1 implies g2 . i = (h1 . (() /. i)) . (f1 . i) )
assume A11: i in dom f1 ; :: thesis: g2 . i = (h1 . (() /. i)) . (f1 . i)
dom f = the carrier of S1 by A1;
then h1 . (() /. i) = h2 . (f . (() /. i)) by
.= h2 . (f . (() . i)) by
.= h2 . ((f * ()) . i) by
.= h2 . (() . i) by A1, A3
.= h2 . (() /. i) by ;
hence g2 . i = (h1 . (() /. i)) . (f1 . i) by ; :: thesis: verum
end;
Args (o2,B2) = Args (o1,(B2 | (S1,f,g))) by A1, A3, Th24;
hence h1 # x1 = h2 # x2 by ; :: thesis: verum