let A, N be non empty finite set ; :: thesis:
let f be Function of Funcs N,(LinOrders A), LinPreorders A; :: thesis:
assume that
A1: for p being Element of Funcs N,(LinOrders A)
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b and
A2: for p, p' being Element of Funcs N,(LinOrders A)
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p' . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p',b ) and
A3: card A >= 3 ; :: thesis:
consider o being Element of LinOrders A;
defpred S₁[ Element of LinPreorders A, Element of A, Element of A] means ( $2 <=_ $1,$3 & ( $2 <_ $1,$3 or $2 <=_ o,$3 ) );
defpred S₂[ Element of LinPreorders A, Element of LinOrders A] means for a, b being Element of A holds
( S₁[$1,a,b] iff a <=_ $2,b );
A4: for o' being Element of LinPreorders A ex o1 being Element of LinOrders A st S₂[o',o1]

proof

let o' be Element of LinPreorders A; :: thesis:
defpred S₃[ Element of A, Element of A] means S₁[o',$1,$2];
consider o1 being Relation of A such that
A5: for a, b being Element of A holds
( [a,b] in o1 iff S₃[a,b] ) from RELSET_1:sch 2();

A6: now

let a, b be Element of A; :: thesis:
( S₃[a,b] or S₃[b,a] ) by Th4;
hence ( [a,b] in o1 or [b,a] in o1 ) by A5; :: thesis:

end;

now

let a, b, c be Element of A; :: thesis:
( S₃[a,b] & S₃[b,c] implies S₃[a,c] ) by Th5;
hence ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 ) by A5; :: thesis:

end;

then reconsider o1 = o1 as Element of LinPreorders A by A6, Def1;

now

let a, b be Element of A; :: thesis:
( S₃[a,b] & S₃[b,a] implies a = b ) by Th6;
hence ( [a,b] in o1 & [b,a] in o1 implies a = b ) by A5; :: thesis:

end;

then reconsider o1 = o1 as Element of LinOrders A by Def2;
take o1 ; :: thesis:
let a, b be Element of A; :: thesis:
( [a,b] in o1 iff S₃[a,b] ) by A5;
hence ( S₁[o',a,b] iff a <=_ o1,b ) by Def4; :: thesis:

end;

defpred S₃[ Element of Funcs N,(LinPreorders A), Element of Funcs N,(LinOrders A)] means for i being Element of N holds S₂[$1 . i,$2 . i];
A7: for q being Element of Funcs N,(LinPreorders A)
for p, p' being Element of Funcs N,(LinOrders A) st S₃[q,p] & S₃[q,p'] holds
p = p'

proof

let q be Element of Funcs N,(LinPreorders A); :: thesis:
let p, p' be Element of Funcs N,(LinOrders A); :: thesis:
assume A8: ( S₃[q,p] & S₃[q,p'] ) ; :: thesis:
let i be Element of N; :: according to FUNCT_2:def 9 :: thesis:
reconsider pi = p . i as Relation of A by Def1;
reconsider pi' = p' . i as Relation of A by Def1;

now

let a, b be Element of A; :: thesis:
( ( S₁[q . i,a,b] implies a <=_ p . i,b ) & ( a <=_ p . i,b implies S₁[q . i,a,b] ) & ( S₁[q . i,a,b] implies a <=_ p' . i,b ) & ( a <=_ p' . i,b implies S₁[q . i,a,b] ) ) by A8;
hence ( [a,b] in p . i iff [a,b] in p' . i ) by Def4; :: thesis:

end;

then pi = pi' by RELSET_1:def 3;
hence p . i = p' . i ; :: thesis:

end;

A9: for q being Element of Funcs N,(LinPreorders A) ex p being Element of Funcs N,(LinOrders A) st S₃[q,p]

proof

let q be Element of Funcs N,(LinPreorders A); :: thesis:
defpred S₄[ Element of N, Element of LinOrders A] means S₂[q . $1,$2];
A10: for i being Element of N ex o1 being Element of LinOrders A st S₄[i,o1] by A4;
consider p being Function of N, LinOrders A such that
A11: for i being Element of N holds S₄[i,p . i] from FUNCT_2:sch 3(A10);
reconsider p = p as Element of Funcs N,(LinOrders A) by FUNCT_2:11;
take p ; :: thesis:
thus S₃[q,p] by A11; :: thesis:

end;

defpred S₄[ Element of Funcs N,(LinPreorders A), Element of LinPreorders A] means ex p being Element of Funcs N,(LinOrders A) st
( S₃[$1,p] & f . p = $2 );
A12: for q being Element of Funcs N,(LinPreorders A) ex o' being Element of LinPreorders A st S₄[q,o']

proof

let q be Element of Funcs N,(LinPreorders A); :: thesis:
consider p being Element of Funcs N,(LinOrders A) such that
A13: S₃[q,p] by A9;
take f . p ; :: thesis:
thus S₄[q,f . p] by A13; :: thesis:

end;

consider f' being Function of Funcs N,(LinPreorders A), LinPreorders A such that
A14: for q being Element of Funcs N,(LinPreorders A) holds S₄[q,f' . q] from FUNCT_2:sch 3(A12);
A15: for q being Element of Funcs N,(LinPreorders A)
for a, b being Element of A st ( for i being Element of N holds a <_ q . i,b ) holds
a <_ f' . q,b

proof

let q be Element of Funcs N,(LinPreorders A); :: thesis:
let a, b be Element of A; :: thesis:
assume A16: for i being Element of N holds a <_ q . i,b ; :: thesis:
consider p being Element of Funcs N,(LinOrders A) such that
A17: ( S₃[q,p] & f . p = f' . q ) by A14;

now

let i be Element of N; :: thesis:
not S₁[q . i,b,a] by A16;
hence a <_ p . i,b by A17; :: thesis:

end;

hence a <_ f' . q,b by A1, A17; :: thesis:

end;

now

let q, q' be Element of Funcs N,(LinPreorders A); :: thesis:
let a, b be Element of A; :: thesis:
assume A18: for i being Element of N holds
( ( a <_ q . i,b implies a <_ q' . i,b ) & ( a <_ q' . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q' . i,a ) & ( b <_ q' . i,a implies b <_ q . i,a ) ) ; :: thesis:
consider p being Element of Funcs N,(LinOrders A) such that
A19: ( S₃[q,p] & f . p = f' . q ) by A14;
consider p' being Element of Funcs N,(LinOrders A) such that
A20: ( S₃[q',p'] & f . p' = f' . q' ) by A14;
for i being Element of N holds
( a <_ p . i,b iff a <_ p' . i,b )

proof

let i be Element of N; :: thesis:
( S₁[q . i,b,a] iff S₁[q' . i,b,a] ) by A18;
hence ( a <_ p . i,b iff a <_ p' . i,b ) by A19, A20; :: thesis:

end;

hence ( a <_ f' . q,b iff a <_ f' . q',b ) by A2, A19, A20; :: thesis:

end;

then consider n being Element of N such that
A21: for q being Element of Funcs N,(LinPreorders A)
for a, b being Element of A st a <_ q . n,b holds
a <_ f' . q,b by A3, A15, Th14;
take n ; :: thesis:
let p be Element of Funcs N,(LinOrders A); :: thesis:

now

rng p c= LinOrders A by RELSET_1:12;
then ( dom p = N & rng p c= LinPreorders A ) by FUNCT_2:def 1, XBOOLE_1:1;
then reconsider q = p as Element of Funcs N,(LinPreorders A) by FUNCT_2:def 2;
A22: S₃[q,p]

proof

let i be Element of N; :: thesis:
let a, b be Element of A; :: thesis:
( a <_ p . i,b or a = b or a >_ p . i,b ) by Th6;
hence ( S₁[q . i,a,b] iff a <=_ p . i,b ) by Th4; :: thesis:

end;

consider p' being Element of Funcs N,(LinOrders A) such that
A23: ( S₃[q,p'] & f . p' = f' . q ) by A14;
let a, b be Element of A; :: thesis:
assume a <_ p . n,b ; :: thesis:
then ( a <_ f' . q,b & p = p' ) by A7, A21, A22, A23;
hence a <_ f . p,b by A23; :: thesis:

end;

hence for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b ) by Th13; :: thesis: