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;

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

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)

Args (o2,B2) = Args (o1,(B2 | (S1,f,g)))
by A1, A3, Th24;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;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

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