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 13 :: 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

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 Th25;

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 Th26;
thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:21
.= (Upsilon F) . (homsym a,a) by A1, Def5
.= homsym (F . a),(F . a) by Th30
.= the_result_sort_of (idsym (F . a)) by Def5
.= the ResultSort of (CatSign the carrier of C2) . ((Psi F) . (idsym a)) by Th31
.= (the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A1, FUNCT_2:21 ; :: 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 Th27;
thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:21
.= (Upsilon F) . (homsym a,c) by A2, Def5
.= homsym (F . a),(F . c) by Th30
.= the_result_sort_of (compsym (F . a),(F . b),(F . c)) by Def5
.= the ResultSort of (CatSign the carrier of C2) . ((Psi F) . (compsym a,b,c)) by Th32
.= (the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A2, FUNCT_2:21 ; :: 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) by FUNCT_2:113; :: 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 o' = 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 ( o' `1 = 1 or o' `1 = 2 ) by Th25;

suppose o' `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 Th26;
( p = {} & (Upsilon F) * {} = {} ) by A3, A4, Def5;
hence (Upsilon F) * p = the_arity_of (idsym (F . a)) by Def5
.= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A4, Th31 ;
:: thesis: verum

end;

suppose o' `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
A5: o = compsym a,b,c by Th27;
( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & p = <*(homsym b,c),(homsym a,b)*> ) by A3, A5, Def5, FUNCT_2:def 1;
hence (Upsilon F) * p = <*((Upsilon F) . (homsym b,c)),((Upsilon F) . (homsym a,b))*> by FINSEQ_2:145
.= <*(homsym (F . b),(F . c)),((Upsilon F) . (homsym a,b))*> by Th30
.= <*(homsym (F . b),(F . c)),(homsym (F . a),(F . b))*> by Th30
.= the_arity_of (compsym (F . a),(F . b),(F . c)) by Def5
.= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A5, Th32 ;
:: thesis: verum

end;

end;