defpred S₁[ object , object ] 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));
set X = (arity o) -tuples_on (Class E);
A1: for e being object st e in (arity o) -tuples_on (Class E) holds
ex u being object st
( u in Class E & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in (arity o) -tuples_on (Class E) implies ex u being object st
( u in Class E & S₁[e,u] ) )
A2: dom o = (arity o) -tuples_on the carrier of U1 by MARGREL1:22
.= { q where q is Element of the carrier of U1 * : len q = arity o } by FINSEQ_2:def 4 ;
assume e in (arity o) -tuples_on (Class E) ; :: thesis: ex u being object st
( u in Class E & S₁[e,u] )
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
A3: s = e and
A4: len s = arity o ;
consider x being FinSequence of the carrier of U1 such that
A5: x is_representatives_FS s by FINSEQ_3:122;
take y = Class (E,(o . x)); :: thesis: ( y in Class E & S₁[e,y] )
A6: len x = arity o by A4, A5, FINSEQ_3:def 4;
x is Element of the carrier of U1 * by FINSEQ_1:def 11;
then A7: x in dom o by A2, A6;
then A8: o . x in rng o by FUNCT_1:def 3;
hence y in Class E by EQREL_1:def 3; :: thesis: S₁[e,y]
let a be FinSequence of Class E; :: thesis: ( a = e implies for x being FinSequence of the carrier of U1 st x is_representatives_FS a holds
y = Class (E,(o . x)) )
assume A9: a = e ; :: thesis: for x being FinSequence of the carrier of U1 st x is_representatives_FS a holds
y = Class (E,(o . x))
let b be FinSequence of the carrier of U1; :: thesis: ( b is_representatives_FS a implies y = Class (E,(o . b)) )
assume A10: b is_representatives_FS a ; :: thesis: y = Class (E,(o . b))
then A11: len b = arity o by A3, A4, A9, FINSEQ_3:def 4;
for m being Nat st m in dom x holds
[(x . m),(b . m)] in E

proof

let m be Nat; :: thesis: ( m in dom x implies [(x . m),(b . m)] in E )
assume A12: m in dom x ; :: thesis: [(x . m),(b . m)] in E
then A13: ( Class (E,(x . m)) = s . m & x . m in rng x ) by A5, FINSEQ_3:def 4, FUNCT_1:def 3;
dom x = Seg (arity o) by A6, FINSEQ_1:def 3
.= dom b by A11, FINSEQ_1:def 3 ;
then Class (E,(b . m)) = s . m by A3, A9, A10, A12, FINSEQ_3:def 4;
hence [(x . m),(b . m)] in E by A13, EQREL_1:35; :: thesis: verum

end;

then A14: [x,b] in ExtendRel E by A6, A11, FINSEQ_3:def 3;
b is Element of the carrier of U1 * by FINSEQ_1:def 11;
then ( ex n being Nat st
( n in dom the charact of U1 & the charact of U1 . n = o ) & b in dom o ) by A2, A11, FINSEQ_2:10;
then [(o . x),(o . b)] in E by A7, A14, Def7;
hence y = Class (E,(o . b)) by A8, EQREL_1:35; :: thesis: verum

end;

consider F being Function such that
A15: ( dom F = (arity o) -tuples_on (Class E) & rng F c= Class E & ( for e being object st e in (arity o) -tuples_on (Class E) holds
S₁[e,F . e] ) ) from FUNCT_1:sch 6(A1);
(arity o) -tuples_on (Class E) in { (m -tuples_on (Class E)) where m is Nat : verum } ;
then (arity o) -tuples_on (Class E) c= union { (m -tuples_on (Class E)) where m is Nat : verum } by ZFMISC_1:74;
then (arity o) -tuples_on (Class E) c= (Class E) * by FINSEQ_2:108;
then reconsider F = F as PartFunc of ((Class E) *),(Class E) by A15, RELSET_1:4;
A16: dom F = { t where t is Element of (Class E) * : len t = arity o } by A15, FINSEQ_2:def 4;
A17: 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: ( len x = len y & x in dom F implies y in dom F )
assume that
A18: len x = len y and
A19: x in dom F ; :: thesis: y in dom F
A20: y is Element of (Class E) * by FINSEQ_1:def 11;
ex t1 being Element of (Class E) * st
( x = t1 & len t1 = arity o ) by A16, A19;
hence y in dom F by A16, A18, A20; :: thesis: verum

end;

A21: ex x being FinSequence st x in dom F

proof

set a = the Element of (arity o) -tuples_on (Class E);
the Element of (arity o) -tuples_on (Class E) in (arity o) -tuples_on (Class E) ;
hence ex x being FinSequence st x in dom F by A15; :: thesis: verum

end;

dom F is with_common_domain

proof

let x, y be FinSequence; :: according to MARGREL1:def 1 :: thesis: ( not x in dom F or not y in dom F or len x = len y )
assume ( x in dom F & y in dom F ) ; :: thesis: len x = len y
then ( ex t1 being Element of (Class E) * st
( x = t1 & len t1 = arity o ) & ex t2 being Element of (Class E) * st
( y = t2 & len t2 = arity o ) ) by A16;
hence len x = len y ; :: thesis: verum

end;

then reconsider F = F as non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) by A17, A21, MARGREL1:def 21, MARGREL1:def 22;
take F ; :: thesis: ( dom F = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x)) ) )
thus dom F = (arity o) -tuples_on (Class E) by A15; :: thesis: for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x))
let y be FinSequence of Class E; :: thesis: ( y in dom F implies for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x)) )
assume A22: y in dom F ; :: thesis: for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x))
let x be FinSequence of the carrier of U1; :: thesis: ( x is_representatives_FS y implies F . y = Class (E,(o . x)) )
assume x is_representatives_FS y ; :: thesis: F . y = Class (E,(o . x))
hence F . y = Class (E,(o . x)) by A15, A22; :: thesis: verum