:: INSTALG1 semantic presentation

theorem Th1: :: INSTALG1:1
canceled;

theorem Th2: :: INSTALG1:2
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being set holds
( b4 is ArgumentSeq of Sym b2,b3 iff b4 is Element of Args b2,(FreeMSA b3) )
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be OperSymbol of c1;
cluster -> DTree-yielding Element of Args a3,(FreeMSA a2);
coherence
for b1 being Element of Args c3,(FreeMSA c2) holds b1 is DTree-yielding
by Th2;
end;

theorem Th3: :: INSTALG1:3
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1 st the Sorts of b2 is_transformable_to the Sorts of b3 holds
for b4 being OperSymbol of b1 st Args b4,b2 <> {} holds
Args b4,b3 <> {}
proof end;

theorem Th4: :: INSTALG1:4
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being Element of Args b2,(FreeMSA b3) holds (Den b2,(FreeMSA b3)) . b4 = [b2,the carrier of b1] -tree b4
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
cluster MSAlgebra(# the Sorts of a2,the Charact of a2 #) -> non-empty ;
coherence
MSAlgebra(# the Sorts of c2,the Charact of c2 #) is non-empty
proof end;
end;

theorem Th5: :: INSTALG1:5
for b1 being non empty non void ManySortedSign
for b2, b3 being MSAlgebra of b1 st MSAlgebra(# the Sorts of b2,the Charact of b2 #) = MSAlgebra(# the Sorts of b3,the Charact of b3 #) holds
for b4 being OperSymbol of b1 holds Den b4,b2 = Den b4,b3 ;

theorem Th6: :: INSTALG1:6
for b1 being non empty non void ManySortedSign
for b2, b3, b4, b5 being MSAlgebra of b1 st MSAlgebra(# the Sorts of b2,the Charact of b2 #) = MSAlgebra(# the Sorts of b4,the Charact of b4 #) & MSAlgebra(# the Sorts of b3,the Charact of b3 #) = MSAlgebra(# the Sorts of b5,the Charact of b5 #) holds
for b6 being ManySortedFunction of b2,b3
for b7 being ManySortedFunction of b4,b5 st b6 = b7 holds
for b8 being OperSymbol of b1 st Args b8,b2 <> {} & Args b8,b3 <> {} holds
for b9 being Element of Args b8,b2
for b10 being Element of Args b8,b4 st b9 = b10 holds
b6 # b9 = b7 # b10
proof end;

theorem Th7: :: INSTALG1:7
for b1 being non empty non void ManySortedSign
for b2, b3, b4, b5 being MSAlgebra of b1 st MSAlgebra(# the Sorts of b2,the Charact of b2 #) = MSAlgebra(# the Sorts of b4,the Charact of b4 #) & MSAlgebra(# the Sorts of b3,the Charact of b3 #) = MSAlgebra(# the Sorts of b5,the Charact of b5 #) & the Sorts of b2 is_transformable_to the Sorts of b3 holds
for b6 being ManySortedFunction of b2,b3 st b6 is_homomorphism b2,b3 holds
ex b7 being ManySortedFunction of b4,b5 st
( b7 = b6 & b7 is_homomorphism b4,b5 )
proof end;

definition
let c1 be ManySortedSign ;
attr a1 is feasible means :Def1: :: INSTALG1:def 1
( the carrier of a1 = {} implies the OperSymbols of a1 = {} );
end;

:: deftheorem Def1 defines feasible INSTALG1:def 1 :
for b1 being ManySortedSign holds
( b1 is feasible iff ( the carrier of b1 = {} implies the OperSymbols of b1 = {} ) );

theorem Th8: :: INSTALG1:8
for b1 being ManySortedSign holds
( b1 is feasible iff dom the ResultSort of b1 = the OperSymbols of b1 )
proof end;

registration
cluster non empty -> feasible ManySortedSign ;
coherence
for b1 being ManySortedSign st not b1 is empty holds
b1 is feasible
proof end;
cluster void -> feasible ManySortedSign ;
coherence
for b1 being ManySortedSign st b1 is void holds
b1 is feasible
proof end;
cluster empty feasible -> void ManySortedSign ;
coherence
for b1 being ManySortedSign st b1 is empty & b1 is feasible holds
b1 is void
proof end;
cluster non void feasible -> non empty ManySortedSign ;
coherence
for b1 being ManySortedSign st not b1 is void & b1 is feasible holds
not b1 is empty
proof end;
end;

registration
cluster non empty non void feasible ManySortedSign ;
existence
ex b1 being ManySortedSign st
( not b1 is void & not b1 is empty )
proof end;
end;

theorem Th9: :: INSTALG1:9
for b1 being feasible ManySortedSign holds id the carrier of b1, id the OperSymbols of b1 form_morphism_between b1,b1
proof end;

theorem Th10: :: INSTALG1:10
for b1, b2 being ManySortedSign
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
( b3 is Function of the carrier of b1,the carrier of b2 & b4 is Function of the OperSymbols of b1,the OperSymbols of b2 )
proof end;

definition
let c1 be feasible ManySortedSign ;
mode Subsignature of c1 -> ManySortedSign means :Def2: :: INSTALG1:def 2
id the carrier of a2, id the OperSymbols of a2 form_morphism_between a2,a1;
existence
ex b1 being ManySortedSign st id the carrier of b1, id the OperSymbols of b1 form_morphism_between b1,c1
proof end;
end;

:: deftheorem Def2 defines Subsignature INSTALG1:def 2 :
for b1 being feasible ManySortedSign
for b2 being ManySortedSign holds
( b2 is Subsignature of b1 iff id the carrier of b2, id the OperSymbols of b2 form_morphism_between b2,b1 );

theorem Th11: :: INSTALG1:11
for b1 being feasible ManySortedSign
for b2 being Subsignature of b1 holds
( the carrier of b2 c= the carrier of b1 & the OperSymbols of b2 c= the OperSymbols of b1 )
proof end;

registration
let c1 be feasible ManySortedSign ;
cluster -> feasible Subsignature of a1;
coherence
for b1 being Subsignature of c1 holds b1 is feasible
proof end;
end;

theorem Th12: :: INSTALG1:12
for b1 being feasible ManySortedSign
for b2 being Subsignature of b1 holds
( the ResultSort of b2 c= the ResultSort of b1 & the Arity of b2 c= the Arity of b1 )
proof end;

theorem Th13: :: INSTALG1:13
for b1 being feasible ManySortedSign
for b2 being Subsignature of b1 holds
( the Arity of b2 = the Arity of b1 | the OperSymbols of b2 & the ResultSort of b2 = the ResultSort of b1 | the OperSymbols of b2 )
proof end;

theorem Th14: :: INSTALG1:14
for b1, b2 being feasible ManySortedSign st the carrier of b2 c= the carrier of b1 & the Arity of b2 c= the Arity of b1 & the ResultSort of b2 c= the ResultSort of b1 holds
b2 is Subsignature of b1
proof end;

theorem Th15: :: INSTALG1:15
for b1, b2 being feasible ManySortedSign st the carrier of b2 c= the carrier of b1 & the Arity of b2 = the Arity of b1 | the OperSymbols of b2 & the ResultSort of b2 = the ResultSort of b1 | the OperSymbols of b2 holds
b2 is Subsignature of b1
proof end;

theorem Th16: :: INSTALG1:16
for b1 being feasible ManySortedSign holds b1 is Subsignature of b1
proof end;

theorem Th17: :: INSTALG1:17
for b1 being feasible ManySortedSign
for b2 being Subsignature of b1
for b3 being Subsignature of b2 holds b3 is Subsignature of b1
proof end;

theorem Th18: :: INSTALG1:18
for b1 being feasible ManySortedSign
for b2 being Subsignature of b1 st b1 is Subsignature of b2 holds
ManySortedSign(# the carrier of b1,the OperSymbols of b1,the Arity of b1,the ResultSort of b1 #) = ManySortedSign(# the carrier of b2,the OperSymbols of b2,the Arity of b2,the ResultSort of b2 #)
proof end;

registration
let c1 be non empty ManySortedSign ;
cluster non empty feasible Subsignature of a1;
existence
not for b1 being Subsignature of c1 holds b1 is empty
proof end;
end;

registration
let c1 be non void feasible ManySortedSign ;
cluster non empty non void feasible Subsignature of a1;
existence
not for b1 being Subsignature of c1 holds b1 is void
proof end;
end;

theorem Th19: :: INSTALG1:19
for b1 being feasible ManySortedSign
for b2 being Subsignature of b1
for b3 being ManySortedSign
for b4, b5 being Function st b4,b5 form_morphism_between b1,b3 holds
b4 | the carrier of b2,b5 | the OperSymbols of b2 form_morphism_between b2,b3
proof end;

theorem Th20: :: INSTALG1:20
for b1 being ManySortedSign
for b2 being feasible ManySortedSign
for b3 being Subsignature of b2
for b4, b5 being Function st b4,b5 form_morphism_between b1,b3 holds
b4,b5 form_morphism_between b1,b2
proof end;

theorem Th21: :: INSTALG1:21
for b1 being ManySortedSign
for b2 being feasible ManySortedSign
for b3 being Subsignature of b2
for b4, b5 being Function st b4,b5 form_morphism_between b1,b2 & rng b4 c= the carrier of b3 & rng b5 c= the OperSymbols of b3 holds
b4,b5 form_morphism_between b1,b3
proof end;

definition
let c1, c2 be non empty ManySortedSign ;
let c3 be MSAlgebra of c2;
let c4, c5 be Function;
assume E15: c4,c5 form_morphism_between c1,c2 ;
func c3 | c1,c4,c5 -> strict MSAlgebra of a1 means :Def3: :: INSTALG1:def 3
( the Sorts of a6 = the Sorts of a3 * a4 & the Charact of a6 = the Charact of a3 * a5 );
existence
ex b1 being strict MSAlgebra of c1 st
( the Sorts of b1 = the Sorts of c3 * c4 & the Charact of b1 = the Charact of c3 * c5 )
proof end;
correctness
uniqueness
for b1, b2 being strict MSAlgebra of c1 st the Sorts of b1 = the Sorts of c3 * c4 & the Charact of b1 = the Charact of c3 * c5 & the Sorts of b2 = the Sorts of c3 * c4 & the Charact of b2 = the Charact of c3 * c5 holds
b1 = b2
;
;
end;

:: deftheorem Def3 defines | INSTALG1:def 3 :
for b1, b2 being non empty ManySortedSign
for b3 being MSAlgebra of b2
for b4, b5 being Function st b4,b5 form_morphism_between b1,b2 holds
for b6 being strict MSAlgebra of b1 holds
( b6 = b3 | b1,b4,b5 iff ( the Sorts of b6 = the Sorts of b3 * b4 & the Charact of b6 = the Charact of b3 * b5 ) );

definition
let c1, c2 be non empty ManySortedSign ;
let c3 be MSAlgebra of c1;
func c3 | c2 -> strict MSAlgebra of a2 equals :: INSTALG1:def 4
a3 | a2,(id the carrier of a2),(id the OperSymbols of a2);
correctness
coherence
c3 | c2,(id the carrier of c2),(id the OperSymbols of c2) is strict MSAlgebra of c2
;
;
end;

:: deftheorem Def4 defines | INSTALG1:def 4 :
for b1, b2 being non empty ManySortedSign
for b3 being MSAlgebra of b1 holds b3 | b2 = b3 | b2,(id the carrier of b2),(id the OperSymbols of b2);

theorem Th22: :: INSTALG1:22
for b1, b2 being non empty ManySortedSign
for b3, b4 being MSAlgebra of b2 st MSAlgebra(# the Sorts of b3,the Charact of b3 #) = MSAlgebra(# the Sorts of b4,the Charact of b4 #) holds
for b5, b6 being Function st b5,b6 form_morphism_between b1,b2 holds
b3 | b1,b5,b6 = b4 | b1,b5,b6
proof end;

theorem Th23: :: INSTALG1:23
for b1, b2 being non empty ManySortedSign
for b3 being non-empty MSAlgebra of b2
for b4, b5 being Function st b4,b5 form_morphism_between b1,b2 holds
b3 | b1,b4,b5 is non-empty
proof end;

registration
let c1 be non empty ManySortedSign ;
let c2 be non empty Subsignature of c1;
let c3 be non-empty MSAlgebra of c1;
cluster a3 | a2 -> strict non-empty ;
coherence
c3 | c2 is non-empty
proof end;
end;

theorem Th24: :: INSTALG1:24
for b1, b2 being non empty non void ManySortedSign
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
for b5 being MSAlgebra of b2
for b6 being OperSymbol of b1
for b7 being OperSymbol of b2 st b7 = b4 . b6 holds
Den b6,(b5 | b1,b3,b4) = Den b7,b5
proof end;

theorem Th25: :: INSTALG1:25
for b1, b2 being non empty non void ManySortedSign
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
for b5 being MSAlgebra of b2
for b6 being OperSymbol of b1
for b7 being OperSymbol of b2 st b7 = b4 . b6 holds
( Args b7,b5 = Args b6,(b5 | b1,b3,b4) & Result b6,(b5 | b1,b3,b4) = Result b7,b5 )
proof end;

theorem Th26: :: INSTALG1:26
for b1 being non empty ManySortedSign
for b2 being MSAlgebra of b1 holds b2 | b1,(id the carrier of b1),(id the OperSymbols of b1) = MSAlgebra(# the Sorts of b2,the Charact of b2 #)
proof end;

theorem Th27: :: INSTALG1:27
for b1 being non empty ManySortedSign
for b2 being MSAlgebra of b1 holds b2 | b1 = MSAlgebra(# the Sorts of b2,the Charact of b2 #) by Th26;

theorem Th28: :: INSTALG1:28
for b1, b2, b3 being non empty ManySortedSign
for b4, b5 being Function st b4,b5 form_morphism_between b1,b2 holds
for b6, b7 being Function st b6,b7 form_morphism_between b2,b3 holds
for b8 being MSAlgebra of b3 holds b8 | b1,(b6 * b4),(b7 * b5) = (b8 | b2,b6,b7) | b1,b4,b5
proof end;

theorem Th29: :: INSTALG1:29
for b1 being non empty feasible ManySortedSign
for b2 being non empty Subsignature of b1
for b3 being non empty Subsignature of b2
for b4 being MSAlgebra of b1 holds b4 | b3 = (b4 | b2) | b3
proof end;

theorem Th30: :: INSTALG1:30
for b1, b2 being non empty ManySortedSign
for b3 being Function of the carrier of b1,the carrier of b2
for b4 being Function st b3,b4 form_morphism_between b1,b2 holds
for b5, b6 being MSAlgebra of b2
for b7 being ManySortedFunction of the Sorts of b5,the Sorts of b6 holds b7 * b3 is ManySortedFunction of the Sorts of (b5 | b1,b3,b4),the Sorts of (b6 | b1,b3,b4)
proof end;

theorem Th31: :: INSTALG1:31
for b1 being non empty ManySortedSign
for b2 being non empty Subsignature of b1
for b3, b4 being MSAlgebra of b1
for b5 being ManySortedFunction of the Sorts of b3,the Sorts of b4 holds b5 | the carrier of b2 is ManySortedFunction of the Sorts of (b3 | b2),the Sorts of (b4 | b2)
proof end;

theorem Th32: :: INSTALG1:32
for b1, b2 being non empty ManySortedSign
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
for b5 being MSAlgebra of b2 holds (id the Sorts of b5) * b3 = id the Sorts of (b5 | b1,b3,b4)
proof end;

theorem Th33: :: INSTALG1:33
for b1 being non empty ManySortedSign
for b2 being non empty Subsignature of b1
for b3 being MSAlgebra of b1 holds (id the Sorts of b3) | the carrier of b2 = id the Sorts of (b3 | b2)
proof end;

theorem Th34: :: INSTALG1:34
for b1, b2 being non empty non void ManySortedSign
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
for b5, b6 being MSAlgebra of b2
for b7 being ManySortedFunction of b5,b6
for b8 being ManySortedFunction of (b5 | b1,b3,b4),(b6 | b1,b3,b4) st b8 = b7 * b3 holds
for b9 being OperSymbol of b1
for b10 being OperSymbol of b2 st b10 = b4 . b9 & Args b10,b5 <> {} & Args b10,b6 <> {} holds
for b11 being Element of Args b10,b5
for b12 being Element of Args b9,(b5 | b1,b3,b4) st b11 = b12 holds
b8 # b12 = b7 # b11
proof end;

theorem Th35: :: INSTALG1:35
for b1, b2 being non empty non void ManySortedSign
for b3, b4 being MSAlgebra of b1 st the Sorts of b3 is_transformable_to the Sorts of b4 holds
for b5 being ManySortedFunction of b3,b4 st b5 is_homomorphism b3,b4 holds
for b6 being Function of the carrier of b2,the carrier of b1
for b7 being Function st b6,b7 form_morphism_between b2,b1 holds
ex b8 being ManySortedFunction of (b3 | b2,b6,b7),(b4 | b2,b6,b7) st
( b8 = b5 * b6 & b8 is_homomorphism b3 | b2,b6,b7,b4 | b2,b6,b7 )
proof end;

theorem Th36: :: INSTALG1:36
for b1 being non void feasible ManySortedSign
for b2 being non void Subsignature of b1
for b3, b4 being MSAlgebra of b1 st the Sorts of b3 is_transformable_to the Sorts of b4 holds
for b5 being ManySortedFunction of b3,b4 st b5 is_homomorphism b3,b4 holds
ex b6 being ManySortedFunction of (b3 | b2),(b4 | b2) st
( b6 = b5 | the carrier of b2 & b6 is_homomorphism b3 | b2,b4 | b2 )
proof end;

theorem Th37: :: INSTALG1:37
for b1, b2 being non empty non void ManySortedSign
for b3 being non-empty MSAlgebra of b1
for b4 being Function of the carrier of b2,the carrier of b1
for b5 being Function st b4,b5 form_morphism_between b2,b1 holds
for b6 being non-empty MSAlgebra of b2 st b6 = b3 | b2,b4,b5 holds
for b7, b8 being SortSymbol of b2
for b9 being Function st b9 is_e.translation_of b6,b7,b8 holds
b9 is_e.translation_of b3,b4 . b7,b4 . b8
proof end;

Lemma26: for b1, b2 being non empty non void ManySortedSign
for b3 being non-empty MSAlgebra of b1
for b4 being Function of the carrier of b2,the carrier of b1
for b5 being Function st b4,b5 form_morphism_between b2,b1 holds
for b6 being non-empty MSAlgebra of b2 st b6 = b3 | b2,b4,b5 holds
for b7, b8 being SortSymbol of b2 st TranslationRel b2 reduces b7,b8 holds
( TranslationRel b1 reduces b4 . b7,b4 . b8 & ( for b9 being Translation of b6,b7,b8 holds b9 is Translation of b3,b4 . b7,b4 . b8 ) )
proof end;

theorem Th38: :: INSTALG1:38
for b1, b2 being non empty non void ManySortedSign
for b3 being Function of the carrier of b2,the carrier of b1
for b4 being Function st b3,b4 form_morphism_between b2,b1 holds
for b5, b6 being SortSymbol of b2 st TranslationRel b2 reduces b5,b6 holds
TranslationRel b1 reduces b3 . b5,b3 . b6
proof end;

theorem Th39: :: INSTALG1:39
for b1, b2 being non empty non void ManySortedSign
for b3 being non-empty MSAlgebra of b1
for b4 being Function of the carrier of b2,the carrier of b1
for b5 being Function st b4,b5 form_morphism_between b2,b1 holds
for b6 being non-empty MSAlgebra of b2 st b6 = b3 | b2,b4,b5 holds
for b7, b8 being SortSymbol of b2 st TranslationRel b2 reduces b7,b8 holds
for b9 being Translation of b6,b7,b8 holds b9 is Translation of b3,b4 . b7,b4 . b8 by Lemma26;

scheme :: INSTALG1:sch 1
s1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> V3 ManySortedSet of the carrier of F1(), F4( set , set ) -> set } :
ex b1 being ManySortedFunction of (FreeMSA F3()),F2() st
( b1 is_homomorphism FreeMSA F3(),F2() & ( for b2 being SortSymbol of F1()
for b3 being Element of F3() . b2 holds (b1 . b2) . (root-tree [b3,b2]) = F4(b3,b2) ) )
provided
E27: for b1 being SortSymbol of F1()
for b2 being Element of F3() . b1 holds F4(b2,b1) in the Sorts of F2() . b1
proof end;

theorem Th40: :: INSTALG1:40
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being ManySortedSubset of b2
for b5 being ManySortedFunction of b2,b3
for b6 being set st b6 in b1 holds
for b7, b8 being Function st b7 = b5 . b6 & b8 = (b5 || b4) . b6 holds
for b9 being set st b9 in b4 . b6 holds
b8 . b9 = b7 . b9
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
cluster FreeGen a2 -> V3 ;
coherence
FreeGen c2 is non-empty
;
end;

definition
let c1, c2 be non empty non void ManySortedSign ;
let c3 be V3 ManySortedSet of the carrier of c2;
let c4 be Function of the carrier of c1,the carrier of c2;
let c5 be Function;
assume E28: c4,c5 form_morphism_between c1,c2 ;
func hom c4,c5,c3,c1,c2 -> ManySortedFunction of (FreeMSA (a3 * a4)),((FreeMSA a3) | a1,a4,a5) means :Def5: :: INSTALG1:def 5
( a6 is_homomorphism FreeMSA (a3 * a4),(FreeMSA a3) | a1,a4,a5 & ( for b1 being SortSymbol of a1
for b2 being Element of (a3 * a4) . b1 holds (a6 . b1) . (root-tree [b2,b1]) = root-tree [b2,(a4 . b1)] ) );
existence
ex b1 being ManySortedFunction of (FreeMSA (c3 * c4)),((FreeMSA c3) | c1,c4,c5) st
( b1 is_homomorphism FreeMSA (c3 * c4),(FreeMSA c3) | c1,c4,c5 & ( for b2 being SortSymbol of c1
for b3 being Element of (c3 * c4) . b2 holds (b1 . b2) . (root-tree [b3,b2]) = root-tree [b3,(c4 . b2)] ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA (c3 * c4)),((FreeMSA c3) | c1,c4,c5) st b1 is_homomorphism FreeMSA (c3 * c4),(FreeMSA c3) | c1,c4,c5 & ( for b3 being SortSymbol of c1
for b4 being Element of (c3 * c4) . b3 holds (b1 . b3) . (root-tree [b4,b3]) = root-tree [b4,(c4 . b3)] ) & b2 is_homomorphism FreeMSA (c3 * c4),(FreeMSA c3) | c1,c4,c5 & ( for b3 being SortSymbol of c1
for b4 being Element of (c3 * c4) . b3 holds (b2 . b3) . (root-tree [b4,b3]) = root-tree [b4,(c4 . b3)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines hom INSTALG1:def 5 :
for b1, b2 being non empty non void ManySortedSign
for b3 being V3 ManySortedSet of the carrier of b2
for b4 being Function of the carrier of b1,the carrier of b2
for b5 being Function st b4,b5 form_morphism_between b1,b2 holds
for b6 being ManySortedFunction of (FreeMSA (b3 * b4)),((FreeMSA b3) | b1,b4,b5) holds
( b6 = hom b4,b5,b3,b1,b2 iff ( b6 is_homomorphism FreeMSA (b3 * b4),(FreeMSA b3) | b1,b4,b5 & ( for b7 being SortSymbol of b1
for b8 being Element of (b3 * b4) . b7 holds (b6 . b7) . (root-tree [b8,b7]) = root-tree [b8,(b4 . b7)] ) ) );

theorem Th41: :: INSTALG1:41
for b1, b2 being non empty non void ManySortedSign
for b3 being V3 ManySortedSet of the carrier of b2
for b4 being Function of the carrier of b1,the carrier of b2
for b5 being Function st b4,b5 form_morphism_between b1,b2 holds
for b6 being OperSymbol of b1
for b7 being Element of Args b6,(FreeMSA (b3 * b4))
for b8 being FinSequence st b8 = (hom b4,b5,b3,b1,b2) # b7 holds
((hom b4,b5,b3,b1,b2) . (the_result_sort_of b6)) . ([b6,the carrier of b1] -tree b7) = [(b5 . b6),the carrier of b2] -tree b8
proof end;

theorem Th42: :: INSTALG1:42
for b1, b2 being non empty non void ManySortedSign
for b3 being V3 ManySortedSet of the carrier of b2
for b4 being Function of the carrier of b1,the carrier of b2
for b5 being Function st b4,b5 form_morphism_between b1,b2 holds
for b6 being Term of b1,(b3 * b4) holds
( ((hom b4,b5,b3,b1,b2) . (the_sort_of b6)) . b6 is CompoundTerm of b2,b3 iff b6 is CompoundTerm of b1,b3 * b4 )
proof end;

theorem Th43: :: INSTALG1:43
for b1, b2 being non empty non void ManySortedSign
for b3 being V3 ManySortedSet of the carrier of b2
for b4 being Function of the carrier of b1,the carrier of b2
for b5 being one-to-one Function st b4,b5 form_morphism_between b1,b2 holds
hom b4,b5,b3,b1,b2 is_monomorphism FreeMSA (b3 * b4),(FreeMSA b3) | b1,b4,b5
proof end;

theorem Th44: :: INSTALG1:44
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1 holds hom (id the carrier of b1),(id the OperSymbols of b1),b2,b1,b1 = id the Sorts of (FreeMSA b2)
proof end;

theorem Th45: :: INSTALG1:45
for b1, b2, b3 being non empty non void ManySortedSign
for b4 being V3 ManySortedSet of the carrier of b3
for b5 being Function of the carrier of b1,the carrier of b2
for b6 being Function st b5,b6 form_morphism_between b1,b2 holds
for b7 being Function of the carrier of b2,the carrier of b3
for b8 being Function st b7,b8 form_morphism_between b2,b3 holds
hom (b7 * b5),(b8 * b6),b4,b1,b3 = ((hom b7,b8,b4,b2,b3) * b5) ** (hom b5,b6,(b4 * b7),b1,b2)
proof end;