let C1, C2 be Category; :: thesis: for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2
let F be Functor of C1,C2; :: thesis: Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2
set f = Upsilon F;
set g = Psi F;
set S1 = CatSign the carrier of C1;
set S2 = CatSign the carrier of C2;
thus ( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & dom (Psi F) = the carrier' of (CatSign the carrier of C1) ) by FUNCT_2:def 1; :: according to PUA2MSS1:def 12 :: thesis: ( proj2 (Upsilon F) c= the carrier of (CatSign the carrier of C2) & proj2 (Psi F) c= the carrier' of (CatSign the carrier of C2) & the ResultSort of (CatSign the carrier of C1) * (Upsilon F) = (Psi F) * the ResultSort of (CatSign the carrier of C2) & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of (CatSign the carrier of C1) or not b₂ = the Arity of (CatSign the carrier of C1) . b₁ or b₂ * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b₁) ) ) )
thus ( rng (Upsilon F) c= the carrier of (CatSign the carrier of C2) & rng (Psi F) c= the carrier' of (CatSign the carrier of C2) ) ; :: thesis: ( the ResultSort of (CatSign the carrier of C1) * (Upsilon F) = (Psi F) * the ResultSort of (CatSign the carrier of C2) & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of (CatSign the carrier of C1) or not b₂ = the Arity of (CatSign the carrier of C1) . b₁ or b₂ * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b₁) ) ) )

now :: thesis: for o being OperSymbol of (CatSign the carrier of C1) holds ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o

let o be OperSymbol of (CatSign the carrier of C1); :: thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b₁ = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b₁

per cases ( o `1 = 1 or o `1 = 2 ) by Th16;

suppose o `1 = 1 ; :: thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b₁ = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b₁

then consider a being Object of C1 such that
A1: o = idsym a by Th17;
thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:15
.= (Upsilon F) . (homsym (a,a)) by A1, Def3
.= homsym ((F . a),(F . a)) by Th21
.= the_result_sort_of (idsym (F . a)) by Def3
.= the ResultSort of (CatSign the carrier of C2) . ((Psi F) . (idsym a)) by Th22
.= ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A1, FUNCT_2:15 ; :: thesis: verum

end;

suppose o `1 = 2 ; :: thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b₁ = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b₁

then consider a, b, c being Object of C1 such that
A2: o = compsym (a,b,c) by Th18;
thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:15
.= (Upsilon F) . (homsym (a,c)) by A2, Def3
.= homsym ((F . a),(F . c)) by Th21
.= the_result_sort_of (compsym ((F . a),(F . b),(F . c))) by Def3
.= the ResultSort of (CatSign the carrier of C2) . ((Psi F) . (compsym (a,b,c))) by Th23
.= ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A2, FUNCT_2:15 ; :: thesis: verum

end;

end;

end;

hence (Upsilon F) * the ResultSort of (CatSign the carrier of C1) = the ResultSort of (CatSign the carrier of C2) * (Psi F) ; :: thesis: for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of (CatSign the carrier of C1) or not b₂ = the Arity of (CatSign the carrier of C1) . b₁ or b₂ * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b₁) )
let o be set ; :: thesis: for b₁ being set holds
( not o in the carrier' of (CatSign the carrier of C1) or not b₁ = the Arity of (CatSign the carrier of C1) . o or b₁ * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) )
let p be Function; :: thesis: ( not o in the carrier' of (CatSign the carrier of C1) or not p = the Arity of (CatSign the carrier of C1) . o or p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) )
assume o in the carrier' of (CatSign the carrier of C1) ; :: thesis: ( not p = the Arity of (CatSign the carrier of C1) . o or p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) )
then reconsider o9 = o as OperSymbol of (CatSign the carrier of C1) ;
assume A3: p = the Arity of (CatSign the carrier of C1) . o ; :: thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o)

per cases ( o9 `1 = 1 or o9 `1 = 2 ) by Th16;

suppose o9 `1 = 1 ; :: thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o)

then consider a being Object of C1 such that
A4: o = idsym a by Th17;
A5: (Upsilon F) * {} = {} ;
p = {} by A3, A4, Def3;
hence (Upsilon F) * p = the_arity_of (idsym (F . a)) by A5, Def3
.= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A4, Th22 ;
:: thesis: verum

end;

suppose o9 `1 = 2 ; :: thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o)

then consider a, b, c being Object of C1 such that
A6: o = compsym (a,b,c) by Th18;
( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & p = <*(homsym (b,c)),(homsym (a,b))*> ) by A3, A6, Def3, FUNCT_2:def 1;
hence (Upsilon F) * p = <*((Upsilon F) . (homsym (b,c))),((Upsilon F) . (homsym (a,b)))*> by FINSEQ_2:125
.= <*(homsym ((F . b),(F . c))),((Upsilon F) . (homsym (a,b)))*> by Th21
.= <*(homsym ((F . b),(F . c))),(homsym ((F . a),(F . b)))*> by Th21
.= the_arity_of (compsym ((F . a),(F . b),(F . c))) by Def3
.= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A6, Th23 ;
:: thesis: verum

end;

end;