set F = F₃();
thus the ObjectMap of F₃() is one-to-one :: according to FUNCTOR0:def 7,FUNCTOR0:def 34,FUNCTOR0:def 36 :: thesis: ( F₃() is faithful & F₃() is V184(F₁(),F₂()) )

proof

let x1, x2, y1, y2 be Element of F₁(); :: according to YELLOW18:def 1 :: thesis: ( the ObjectMap of F₃() . x1,y1 = the ObjectMap of F₃() . x2,y2 implies ( x1 = x2 & y1 = y2 ) )
reconsider a1 = x1, a2 = x2, b1 = y1, b2 = y2 as object of F₁() ;
assume the ObjectMap of F₃() . x1,y1 = the ObjectMap of F₃() . x2,y2 ; :: thesis: ( x1 = x2 & y1 = y2 )
then [(F₃() . b1),(F₃() . a1)] = the ObjectMap of F₃() . x2,y2 by FUNCTOR0:24
.= [(F₃() . b2),(F₃() . a2)] by FUNCTOR0:24 ;
then ( F₃() . a1 = F₃() . a2 & F₃() . b1 = F₃() . b2 ) by ZFMISC_1:33;
then ( F₄(a1) = F₃() . a2 & F₄(b1) = F₃() . b2 ) by A1;
then ( F₄(a1) = F₄(a2) & F₄(b1) = F₄(b2) ) by A1;
hence ( x1 = x2 & y1 = y2 ) by A3; :: thesis: verum

end;

now

let i be set ; :: thesis: ( i in [:the carrier of F₁(),the carrier of F₁():] implies the MorphMap of F₃() . i is one-to-one )
assume i in [:the carrier of F₁(),the carrier of F₁():] ; :: thesis: the MorphMap of F₃() . i is one-to-one
then consider a, b being set such that
A6: ( a in the carrier of F₁() & b in the carrier of F₁() & i = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F₁() by A6;
A7: ( <^a,b^> <> {} implies <^(F₃() . b),(F₃() . a)^> <> {} ) by FUNCTOR0:def 20;
Morph-Map F₃(),a,b is one-to-one

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 (Morph-Map F₃(),a,b) or not y in proj1 (Morph-Map F₃(),a,b) or not (Morph-Map F₃(),a,b) . x = (Morph-Map F₃(),a,b) . y or x = y )
assume A8: ( x in dom (Morph-Map F₃(),a,b) & y in dom (Morph-Map F₃(),a,b) ) ; :: thesis: ( not (Morph-Map F₃(),a,b) . x = (Morph-Map F₃(),a,b) . y or x = y )
then reconsider f = x, g = y as Morphism of a,b ;
( F₃() . f = (Morph-Map F₃(),a,b) . x & F₃() . g = (Morph-Map F₃(),a,b) . y ) by A7, A8, FUNCTOR0:def 17;
then ( F₅(a,b,f) = (Morph-Map F₃(),a,b) . x & F₅(a,b,g) = (Morph-Map F₃(),a,b) . y ) by A2, A8;
hence ( not (Morph-Map F₃(),a,b) . x = (Morph-Map F₃(),a,b) . y or x = y ) by A4, A8; :: thesis: verum

end;

hence the MorphMap of F₃() . i is one-to-one by A6; :: thesis: verum

end;

hence the MorphMap of F₃() is "1-1" by MSUALG_3:1; :: according to FUNCTOR0:def 31 :: thesis: F₃() is V184(F₁(),F₂())
reconsider G = the MorphMap of F₃() as ManySortedFunction of the Arrows of F₁(),the Arrows of F₂() * the ObjectMap of F₃() by FUNCTOR0:def 5;
thus F₃() is full :: according to FUNCTOR0:def 35 :: thesis: F₃() is onto

proof

take G ; :: according to FUNCTOR0:def 33 :: thesis: ( G = the MorphMap of F₃() & G is "onto" )
thus G = the MorphMap of F₃() ; :: thesis: G is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [:the carrier of F₁(),the carrier of F₁():] or proj2 (G . i) = (the ObjectMap of F₃() * the Arrows of F₂()) . i )
assume i in [:the carrier of F₁(),the carrier of F₁():] ; :: thesis: proj2 (G . i) = (the ObjectMap of F₃() * the Arrows of F₂()) . i
then reconsider ab = i as Element of [:the carrier of F₁(),the carrier of F₁():] ;
G . ab is Function of (the Arrows of F₁() . ab),((the Arrows of F₂() * the ObjectMap of F₃()) . ab) ;
hence rng (G . i) c= (the Arrows of F₂() * the ObjectMap of F₃()) . i by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: (the ObjectMap of F₃() * the Arrows of F₂()) . i c= proj2 (G . i)
consider a, b being set such that
A9: ( a in the carrier of F₁() & b in the carrier of F₁() & ab = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F₁() by A9;
A10: the ObjectMap of F₃() . ab = the ObjectMap of F₃() . a,b by A9
.= [(F₃() . b),(F₃() . a)] by FUNCTOR0:24 ;
then A11: (the Arrows of F₂() * the ObjectMap of F₃()) . ab = <^(F₃() . b),(F₃() . a)^> by FUNCT_2:21;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (the ObjectMap of F₃() * the Arrows of F₂()) . i or x in proj2 (G . i) )
assume A12: x in (the Arrows of F₂() * the ObjectMap of F₃()) . i ; :: thesis: x in proj2 (G . i)
then reconsider f = x as Morphism of (F₃() . b),(F₃() . a) by A10, FUNCT_2:21;
consider c, d being object of F₁(), g being Morphism of c,d such that
A13: ( F₃() . a = F₄(c) & F₃() . b = F₄(d) & <^c,d^> <> {} & f = F₅(c,d,g) ) by A5, A11, A12;
( F₄(a) = F₄(c) & F₄(b) = F₄(d) ) by A1, A13;
then A14: ( a = c & b = d ) by A3;
A15: f = F₃() . g by A2, A13
.= (Morph-Map F₃(),c,d) . g by A11, A12, A13, A14, FUNCTOR0:def 17 ;
( dom (Morph-Map F₃(),a,b) = <^a,b^> & G . ab = Morph-Map F₃(),a,b ) by A9, A11, A12, FUNCT_2:def 1;
hence x in proj2 (G . i) by A13, A14, A15, FUNCT_1:def 5; :: thesis: verum

end;

thus rng the ObjectMap of F₃() c= [:the carrier of F₂(),the carrier of F₂():] ; :: according to FUNCTOR0:def 8,FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: [:the carrier of F₂(),the carrier of F₂():] c= proj2 the ObjectMap of F₃()
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:the carrier of F₂(),the carrier of F₂():] or x in proj2 the ObjectMap of F₃() )
assume x in [:the carrier of F₂(),the carrier of F₂():] ; :: thesis: x in proj2 the ObjectMap of F₃()
then consider a, b being set such that
A16: ( a in the carrier of F₂() & b in the carrier of F₂() & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F₂() by A16;
consider c, c' being object of F₁(), g being Morphism of c,c' such that
A17: ( a = F₄(c) & a = F₄(c') & <^c,c'^> <> {} & idm a = F₅(c,c',g) ) by A5;
consider d, d' being object of F₁(), h being Morphism of d,d' such that
A18: ( b = F₄(d) & b = F₄(d') & <^d,d'^> <> {} & idm b = F₅(d,d',h) ) by A5;
[d,c] in [:the carrier of F₁(),the carrier of F₁():] by ZFMISC_1:def 2;
then A19: [d,c] in dom the ObjectMap of F₃() by FUNCT_2:def 1;
the ObjectMap of F₃() . [d,c] = the ObjectMap of F₃() . d,c
.= [(F₃() . c),(F₃() . d)] by FUNCTOR0:24
.= [a,(F₃() . d)] by A1, A17
.= x by A1, A16, A18 ;
hence x in proj2 the ObjectMap of F₃() by A19, FUNCT_1:def 5; :: thesis: verum