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 V189(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 A6: [(F₃() . b1),(F₃() . a1)] = the ObjectMap of F₃() . x2,y2 by FUNCTOR0:24
.= [(F₃() . b2),(F₃() . a2)] by FUNCTOR0:24 ;
then A7: F₃() . a1 = F₃() . a2 by ZFMISC_1:33;
A8: F₃() . b1 = F₃() . b2 by A6, ZFMISC_1:33;
A9: F₄(a1) = F₃() . a2 by A1, A7;
A10: F₄(b1) = F₃() . b2 by A1, A8;
A11: F₄(a1) = F₄(a2) by A1, A9;
F₄(b1) = F₄(b2) by A1, A10;
hence ( x1 = x2 & y1 = y2 ) by A3, A11; :: 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
A12: a in the carrier of F₁() and
A13: b in the carrier of F₁() and
A14: i = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F₁() by A12, A13;
A15: ( <^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 that
A16: x in dom (Morph-Map F₃(),a,b) and
A17: 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 )
reconsider f = x, g = y as Morphism of a,b by A16, A17;
A18: F₃() . f = (Morph-Map F₃(),a,b) . x by A15, A16, FUNCTOR0:def 17;
A19: F₃() . g = (Morph-Map F₃(),a,b) . y by A15, A16, FUNCTOR0:def 17;
A20: F₅(a,b,f) = (Morph-Map F₃(),a,b) . x by A2, A16, A18;
F₅(a,b,g) = (Morph-Map F₃(),a,b) . y by A2, A16, A19;
hence ( not (Morph-Map F₃(),a,b) . x = (Morph-Map F₃(),a,b) . y or x = y ) by A4, A16, A20; :: thesis: verum

end;

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

end;

hence the MorphMap of F₃() is "1-1" by MSUALG_3:1; :: according to FUNCTOR0:def 31 :: thesis: F₃() is V189(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
A21: a in the carrier of F₁() and
A22: b in the carrier of F₁() and
A23: ab = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F₁() by A21, A22;
A24: the ObjectMap of F₃() . ab = the ObjectMap of F₃() . a,b by A23
.= [(F₃() . b),(F₃() . a)] by FUNCTOR0:24 ;
then A25: (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 A26: 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 A24, FUNCT_2:21;
consider c, d being object of F₁(), g being Morphism of c,d such that
A27: F₃() . a = F₄(c) and
A28: F₃() . b = F₄(d) and
A29: <^c,d^> <> {} and
A30: f = F₅(c,d,g) by A5, A25, A26;
A31: F₄(a) = F₄(c) by A1, A27;
A32: F₄(b) = F₄(d) by A1, A28;
A33: a = c by A3, A31;
A34: b = d by A3, A32;
A35: f = F₃() . g by A2, A29, A30
.= (Morph-Map F₃(),c,d) . g by A25, A26, A29, A33, A34, FUNCTOR0:def 17 ;
dom (Morph-Map F₃(),a,b) = <^a,b^> by A25, A26, FUNCT_2:def 1;
hence x in proj2 (G . i) by A23, A29, A33, A34, A35, 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
A36: a in the carrier of F₂() and
A37: b in the carrier of F₂() and
A38: x = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F₂() by A36, A37;
consider c, c9 being object of F₁(), g being Morphism of c,c9 such that
A39: a = F₄(c) and
a = F₄(c9) and
<^c,c9^> <> {} and
idm a = F₅(c,c9,g) by A5;
consider d, d9 being object of F₁(), h being Morphism of d,d9 such that
A40: b = F₄(d) and
b = F₄(d9) and
<^d,d9^> <> {} and
idm b = F₅(d,d9,h) by A5;
[d,c] in [:the carrier of F₁(),the carrier of F₁():] by ZFMISC_1:def 2;
then A41: [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, A39
.= x by A1, A38, A40 ;
hence x in proj2 the ObjectMap of F₃() by A41, FUNCT_1:def 5; :: thesis: verum