set X = (arity o) -tuples_on (Class E);
defpred S₁[ set , set ] means for y being FinSequence of Class E st y = $1 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
$2 = Class E,(o . x);
A1: for e being set st e in (arity o) -tuples_on (Class E) holds
ex u being set st
( u in Class E & S₁[e,u] )

proof

let e be set ; :: thesis:
assume e in (arity o) -tuples_on (Class E) ; :: thesis:
then e in { s where s is Element of (Class E) * : len s = arity o } by FINSEQ_2:def 4;
then consider s being Element of (Class E) * such that
A2: ( s = e & len s = arity o ) ;
consider x being FinSequence of the carrier of U1 such that
A3: x is_representatives_FS s by Th19;
take y = Class E,(o . x); :: thesis:
A4: dom o = (arity o) -tuples_on the carrier of U1 by UNIALG_2:2
.= { q where q is Element of the carrier of U1 * : len q = arity o } by FINSEQ_2:def 4 ;
A5: len x = arity o by A2, A3, Def11;
x is Element of the carrier of U1 * by FINSEQ_1:def 11;
then A6: x in dom o by A4, A5;
then A7: ( o . x in rng o & rng o c= the carrier of U1 ) by FUNCT_1:def 5;
hence y in Class E by EQREL_1:def 5; :: thesis:
let a be FinSequence of Class E; :: thesis:
assume A8: a = e ; :: thesis:
let b be FinSequence of the carrier of U1; :: thesis:
assume A9: b is_representatives_FS a ; :: thesis:
consider n being Nat such that
A10: ( n in dom the charact of U1 & the charact of U1 . n = o ) by FINSEQ_2:11;
A11: len b = arity o by A2, A8, A9, Def11;
b is Element of the carrier of U1 * by FINSEQ_1:def 11;
then A12: b in dom o by A4, A11;
for m being Element of NAT st m in dom x holds
[(x . m),(b . m)] in E

proof

let m be Element of NAT ; :: thesis:
assume A13: m in dom x ; :: thesis:
then A14: Class E,(x . m) = s . m by A3, Def11;
dom x = Seg (arity o) by A5, FINSEQ_1:def 3
.= dom b by A11, FINSEQ_1:def 3 ;
then A15: Class E,(b . m) = s . m by A2, A8, A9, A13, Def11;
( x . m in rng x & rng x c= the carrier of U1 ) by A13, FUNCT_1:def 5;
hence [(x . m),(b . m)] in E by A14, A15, EQREL_1:44; :: thesis:

end;

then [x,b] in ExtendRel E by A5, A11, Def9;
then [(o . x),(o . b)] in E by A6, A10, A12, Def10;
hence y = Class E,(o . b) by A7, EQREL_1:44; :: thesis:

end;

consider F being Function such that
A16: ( dom F = (arity o) -tuples_on (Class E) & rng F c= Class E & ( for e being set st e in (arity o) -tuples_on (Class E) holds
S₁[e,F . e] ) ) from WELLORD2:sch 1(A1);
(arity o) -tuples_on (Class E) in { (m -tuples_on (Class E)) where m is Element of NAT : verum } ;
then (arity o) -tuples_on (Class E) c= union { (m -tuples_on (Class E)) where m is Element of NAT : verum } by ZFMISC_1:92;
then (arity o) -tuples_on (Class E) c= (Class E) * by FINSEQ_2:128;
then reconsider F = F as PartFunc of ((Class E) * ),(Class E) by A16, RELSET_1:11;
A17: dom F = { t where t is Element of (Class E) * : len t = arity o } by A16, FINSEQ_2:def 4;
A18: ( ex x being FinSequence st x in dom F & ( for x, y being FinSequence st x in dom F & y in dom F holds
len x = len y ) )

proof

consider a being Element of (arity o) -tuples_on (Class E);
a in (arity o) -tuples_on (Class E) ;
hence ex x being FinSequence st x in dom F by A16; :: thesis:
let x, y be FinSequence; :: thesis:
assume A19: ( x in dom F & y in dom F ) ; :: thesis:
then consider t1 being Element of (Class E) * such that
A20: ( x = t1 & len t1 = arity o ) by A17;
consider t2 being Element of (Class E) * such that
A21: ( y = t2 & len t2 = arity o ) by A17, A19;
thus len x = len y by A20, A21; :: thesis:

end;

for x, y being FinSequence of Class E st len x = len y & x in dom F holds
y in dom F

proof

let x, y be FinSequence of Class E; :: thesis:
assume A22: ( len x = len y & x in dom F ) ; :: thesis:
then consider t1 being Element of (Class E) * such that
A23: ( x = t1 & len t1 = arity o ) by A17;
y is Element of (Class E) * by FINSEQ_1:def 11;
hence y in dom F by A17, A22, A23; :: thesis:

end;

then reconsider F = F as non empty homogeneous quasi_total PartFunc of ((Class E) * ),(Class E) by A18, UNIALG_1:def 1, UNIALG_1:def 2;
take F ; :: thesis:
thus dom F = (arity o) -tuples_on (Class E) by A16; :: thesis:
let y be FinSequence of Class E; :: thesis:
assume A24: y in dom F ; :: thesis:
let x be FinSequence of the carrier of U1; :: thesis:
assume x is_representatives_FS y ; :: thesis:
hence F . y = Class E,(o . x) by A16, A24; :: thesis: