let C be category; ( 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)) )
( ( 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
C such that A1:
for
a1,
a2 being
Object of
C holds
<^a1,a2^> c= Funcs (
(F . a1),
(F . a2))
;
YELLOW18:def 7 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;
<^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2))
A2:
idm a1 in <^a1,a1^>
;
A3:
<^a1,a1^> c= Funcs (
(F . a1),
(F . a1))
by A1;
A4:
<^a2,a2^> c= Funcs (
(F . a2),
(F . a2))
by A1;
A5:
idm a2 in <^a2,a2^>
;
A6:
ex
f1 being
Function st
(
idm a1 = f1 &
dom f1 = F . a1 &
rng f1 c= F . a1 )
by A2, A3, FUNCT_2:def 2;
ex
f2 being
Function st
(
idm a2 = f2 &
dom f2 = F . a2 &
rng f2 c= F . a2 )
by A4, A5, FUNCT_2:def 2;
hence
<^a1,a2^> c= Funcs (
(the_carrier_of a1),
(the_carrier_of a2))
by A1, A6;
verum
end;
assume A7:
for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2))
; C is para-functional
deffunc H1( set ) -> set = C -carrier_of $1;
consider F being ManySortedSet of the carrier of C such that
A8:
for a being Element of C holds F . a = H1(a)
from PBOOLE:sch 5();
take
F
; YELLOW18:def 7 for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2))
let a, b be Object of C; <^a,b^> c= Funcs ((F . a),(F . b))
A9:
F . a = the_carrier_of a
by A8;
F . b = the_carrier_of b
by A8;
hence
<^a,b^> c= Funcs ((F . a),(F . b))
by A7, A9; verum