let C be category; :: thesis: ( C is para-functional iff for a1, a2 being object of C holds <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2) )
thus
( C is para-functional implies for a1, a2 being object of C holds <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2) )
:: thesis: ( ( for a1, a2 being object of C holds <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2) ) implies C is para-functional )proof
given F being
ManySortedSet of
such that A1:
for
a1,
a2 being
object of
C holds
<^a1,a2^> c= Funcs (F . a1),
(F . a2)
;
:: according to YELLOW18:def 7 :: thesis: for a1, a2 being object of C holds <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2)
let a1,
a2 be
object of
C;
:: thesis: <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2)
A2:
(
idm a1 in <^a1,a1^> &
<^a1,a1^> c= Funcs (F . a1),
(F . a1) &
<^a2,a2^> c= Funcs (F . a2),
(F . a2) &
idm a2 in <^a2,a2^> )
by A1;
then consider f1 being
Function such that A3:
(
idm a1 = f1 &
dom f1 = F . a1 &
rng f1 c= F . a1 )
by FUNCT_2:def 2;
consider f2 being
Function such that A4:
(
idm a2 = f2 &
dom f2 = F . a2 &
rng f2 c= F . a2 )
by A2, FUNCT_2:def 2;
(
the_carrier_of a1 = F . a1 &
the_carrier_of a2 = F . a2 )
by A3, A4;
hence
<^a1,a2^> c= Funcs (the_carrier_of a1),
(the_carrier_of a2)
by A1;
:: thesis: verum
end;
assume A5:
for a1, a2 being object of C holds <^a1,a2^> c= Funcs (the_carrier_of a1),(the_carrier_of a2)
; :: thesis: C is para-functional
deffunc H1( set ) -> set = C -carrier_of $1;
consider F being ManySortedSet of such that
A6:
for a being Element of C holds F . a = H1(a)
from PBOOLE:sch 5();
take
F
; :: according to YELLOW18:def 7 :: thesis: for a1, a2 being object of C holds <^a1,a2^> c= Funcs (F . a1),(F . a2)
let a, b be object of C; :: thesis: <^a,b^> c= Funcs (F . a),(F . b)
( F . a = the_carrier_of a & F . b = the_carrier_of b )
by A6;
hence
<^a,b^> c= Funcs (F . a),(F . b)
by A5; :: thesis: verum