:: Institution of Many-sorted Algebras, Part { I } : Signature Reduct of an Algebra
:: by Grzegorz Bancerek
::
:: Received December 30, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

theorem Th1: :: INSTALG1:1
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V16() ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )
proofend;

registration
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
cluster  ->  DTree-yielding for Element of Args (o,(FreeMSA V));
coherence
 for b1 being Element of Args (o,(FreeMSA V)) holds b1 is DTree-yielding by Th1;
end;

theorem Th2: :: INSTALG1:2
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}
proofend;

theorem Th3: :: INSTALG1:3
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V16() ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
proofend;

theorem :: INSTALG1:4
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for o being OperSymbol of S holds Den (o,A) = Den (o,B) ;

theorem Th5: :: INSTALG1:5
for S being non empty non void ManySortedSign
for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) &amp; MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g holds
for o being OperSymbol of S st Args (o,A1) <> {} &amp; Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
proofend;

theorem :: INSTALG1:6
for S being non empty non void ManySortedSign
for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) &amp; MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) &amp; the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h &amp; h9 is_homomorphism B1,B2 )
proofend;

definition
let S be ManySortedSign ;
attrS is feasible  means :Def1: :: INSTALG1:def 1
( the carrier of S = {} implies the carrier' of S = {} );
end;

:: deftheorem Def1 defines feasible INSTALG1:def_1_:_
 for S being ManySortedSign holds
( S is feasible iff ( the carrier of S = {} implies the carrier' of S = {} ) );

theorem Th7: :: INSTALG1:7
for S being ManySortedSign holds
( S is feasible iff dom the ResultSort of S = the carrier' of S )
proofend;

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

registration
cluster non empty non void for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( not b1 is void &amp; not b1 is empty )
proofend;
end;

theorem Th8: :: INSTALG1:8
for S being feasible ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proofend;

theorem Th9: :: INSTALG1:9
for S1, S2 being ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
( f is Function of the carrier of S1, the carrier of S2 &amp; g is Function of the carrier' of S1, the carrier' of S2 )
proofend;

begin

definition
let S be feasible ManySortedSign ;
mode Subsignature of S ->  ManySortedSign  means :Def2: :: INSTALG1:def 2
 id the carrier of it, id the carrier' of it form_morphism_between it,S;
existence
 ex b1 being ManySortedSign st id the carrier of b1, id the carrier' of b1 form_morphism_between b1,S
proofend;
end;

:: deftheorem Def2 defines Subsignature INSTALG1:def_2_:_
 for S being feasible ManySortedSign
for b2 being ManySortedSign holds
( b2 is Subsignature of S iff id the carrier of b2, id the carrier' of b2 form_morphism_between b2,S );

theorem Th10: :: INSTALG1:10
for S being feasible ManySortedSign
for T being Subsignature of S holds
( the carrier of T c= the carrier of S &amp; the carrier' of T c= the carrier' of S )
proofend;

registration
let S be feasible ManySortedSign ;
cluster  ->  feasible for Subsignature of S;
coherence
 for b1 being Subsignature of S holds b1 is feasible
proofend;
end;

theorem Th11: :: INSTALG1:11
for S being feasible ManySortedSign
for T being Subsignature of S holds
( the ResultSort of T c= the ResultSort of S &amp; the Arity of T c= the Arity of S )
proofend;

theorem Th12: :: INSTALG1:12
for S being feasible ManySortedSign
for T being Subsignature of S holds
( the Arity of T = the Arity of S | the carrier' of T &amp; the ResultSort of T = the ResultSort of S | the carrier' of T )
proofend;

theorem Th13: :: INSTALG1:13
for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S &amp; the Arity of T c= the Arity of S &amp; the ResultSort of T c= the ResultSort of S holds
T is Subsignature of S
proofend;

theorem :: INSTALG1:14
for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S &amp; the Arity of T = the Arity of S | the carrier' of T &amp; the ResultSort of T = the ResultSort of S | the carrier' of T holds
T is Subsignature of S
proofend;

theorem Th15: :: INSTALG1:15
for S being feasible ManySortedSign holds S is Subsignature of S
proofend;

theorem :: INSTALG1:16
for S1 being feasible ManySortedSign
for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1
proofend;

theorem :: INSTALG1:17
for S1 being feasible ManySortedSign
for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
proofend;

registration
let S be non empty ManySortedSign ;
cluster non empty feasible for Subsignature of S;
existence
 not for b1 being Subsignature of S holds b1 is empty
proofend;
end;

registration
let S be non void feasible ManySortedSign ;
cluster non void feasible for Subsignature of S;
existence
 not for b1 being Subsignature of S holds b1 is void
proofend;
end;

theorem :: INSTALG1:18
for S being feasible ManySortedSign
for S9 being Subsignature of S
for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
proofend;

theorem :: INSTALG1:19
for S being ManySortedSign
for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
proofend;

theorem :: INSTALG1:20
for S being ManySortedSign
for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T &amp; rng f c= the carrier of T9 &amp; rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9
proofend;

begin

definition
let S1, S2 be non empty ManySortedSign ;
let A be MSAlgebra over S2;
let f, g be Function;
assume B1: f,g form_morphism_between S1,S2 ;
funcA | (S1,f,g) ->  strict MSAlgebra over S1 means :Def3: :: INSTALG1:def 3
( the Sorts of it = the Sorts of A * f &amp; the Charact of it = the Charact of A * g );
existence
 ex b1 being strict MSAlgebra over S1 st
( the Sorts of b1 = the Sorts of A * f &amp; the Charact of b1 = the Charact of A * g )
proofend;
correctness
uniqueness
for b1, b2 being strict MSAlgebra over S1 st the Sorts of b1 = the Sorts of A * f &amp; the Charact of b1 = the Charact of A * g &amp; the Sorts of b2 = the Sorts of A * f &amp; the Charact of b2 = the Charact of A * g holds
b1 = b2;
;
end;

:: deftheorem Def3 defines | INSTALG1:def_3_:_
 for S1, S2 being non empty ManySortedSign
for A being MSAlgebra over S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
for b6 being strict MSAlgebra over S1 holds
( b6 = A | (S1,f,g) iff ( the Sorts of b6 = the Sorts of A * f &amp; the Charact of b6 = the Charact of A * g ) );

definition
let S2, S1 be non empty ManySortedSign ;
let A be MSAlgebra over S2;
funcA | S1 ->  strict MSAlgebra over S1 equals :: INSTALG1:def 4
A | (S1,(id the carrier of S1),(id the carrier' of S1));
correctness
coherence
A | (S1,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1;
;
end;

:: deftheorem  defines | INSTALG1:def_4_:_
 for S2, S1 being non empty ManySortedSign
for A being MSAlgebra over S2 holds A | S1 = A | (S1,(id the carrier of S1),(id the carrier' of S1));

theorem :: INSTALG1:21
for S1, S2 being non empty ManySortedSign
for A, B being MSAlgebra over S2 st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g)
proofend;

theorem Th22: :: INSTALG1:22
for S1, S2 being non empty ManySortedSign
for A being non-empty MSAlgebra over S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) is non-empty
proofend;

registration
let S2 be non empty ManySortedSign ;
let S1 be non empty Subsignature of S2;
let A be non-empty MSAlgebra over S2;
clusterA | S1 ->  strict non-empty ;
coherence
 A | S1 is non-empty
proofend;
end;

theorem Th23: :: INSTALG1:23
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
proofend;

theorem Th24: :: INSTALG1:24
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) &amp; Result (o1,(A | (S1,f,g))) = Result (o2,A) )
proofend;

theorem Th25: :: INSTALG1:25
for S being non empty ManySortedSign
for A being MSAlgebra over S holds A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #)
proofend;

theorem :: INSTALG1:26
for S being non empty ManySortedSign
for A being MSAlgebra over S holds A | S = MSAlgebra(# the Sorts of A, the Charact of A #) by Th25;

theorem Th27: :: INSTALG1:27
for S1, S2, S3 being non empty ManySortedSign
for f1, g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
proofend;

theorem :: INSTALG1:28
for S1 being non empty feasible ManySortedSign
for S2 being non empty Subsignature of S1
for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
proofend;

theorem Th29: :: INSTALG1:29
for S1, S2 being non empty ManySortedSign
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
proofend;

theorem :: INSTALG1:30
for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
proofend;

theorem Th31: :: INSTALG1:31
for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
proofend;

theorem :: INSTALG1:32
for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)
proofend;

theorem Th33: :: INSTALG1:33
for S1, S2 being non empty non void ManySortedSign
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 &amp; Args (o2,A) <> {} &amp; 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
proofend;

theorem Th34: :: INSTALG1:34
for S, S9 being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f &amp; h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
proofend;

theorem :: INSTALG1:35
for S being non void feasible ManySortedSign
for S9 being non void Subsignature of S
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 &amp; h9 is_homomorphism A1 | S9,A2 | S9 )
proofend;

theorem Th36: :: INSTALG1:36
for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
proofend;

Lm1:  for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 &amp; ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
proofend;

theorem :: INSTALG1:37
for S, S9 being non empty non void ManySortedSign
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
proofend;

theorem :: INSTALG1:38
for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 by Lm1;

begin

scheme :: INSTALG1:sch 1
GenFuncEx{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3() ->  V16() ManySortedSet of the carrier of F1(), F4( set , set ) ->  set } :
 ex h being ManySortedFunction of (FreeMSA F3()),F2() st
( h is_homomorphism FreeMSA F3(),F2() &amp; ( for s being SortSymbol of F1()
for x being Element of F3() . s holds (h . s) . (root-tree [x,s]) = F4(x,s) ) )
provided
A1: for s being SortSymbol of F1()
for x being Element of F3() . s holds F4(x,s) in the Sorts of F2() . s
proofend;

theorem Th39: :: INSTALG1:39
for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i &amp; g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
proofend;

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster FreeGen X -> V16() ;
coherence
 FreeGen X is non-empty ;
end;

definition
let S1, S2 be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function;
assume B1: f,g form_morphism_between S1,S2 ;
func hom (f,g,X,S1,S2) ->  ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) means :Def5: :: INSTALG1:def 5
( it is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) &amp; ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (it . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) );
existence
 ex b1 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st
( b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) &amp; ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) &amp; ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) &amp; b2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) &amp; ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines hom INSTALG1:def_5_:_
 for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for b6 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) holds
( b6 = hom (f,g,X,S1,S2) iff ( b6 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) &amp; ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b6 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );

theorem Th40: :: INSTALG1:40
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
proofend;

theorem Th41: :: INSTALG1:41
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
proofend;

theorem :: INSTALG1:42
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being one-to-one Function st f,g form_morphism_between S1,S2 holds
hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)
proofend;

theorem :: INSTALG1:43
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)
proofend;

theorem :: INSTALG1:44
for S1, S2, S3 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S3
for f1 being Function of the carrier of S1, the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
proofend;