defpred S1[ 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 & S1[e,u] )
proof
let e be
object ;
( e in (arity o) -tuples_on (Class E) implies ex u being object st
( u in Class E & S1[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)
;
ex u being object st
( u in Class E & S1[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));
( y in Class E & S1[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;
S1[e,y]
let a be
FinSequence of
Class E;
( 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
;
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;
( b is_representatives_FS a implies y = Class (E,(o . b)) )
assume A10:
b is_representatives_FS a
;
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;
( m in dom x implies [(x . m),(b . m)] in E )
assume A12:
m in dom x
;
[(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;
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;
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
S1[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
A21:
ex x being FinSequence st x in dom F
dom F is with_common_domain
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
; ( 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; 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; ( 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
; 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; ( x is_representatives_FS y implies F . y = Class (E,(o . x)) )
assume
x is_representatives_FS y
; F . y = Class (E,(o . x))
hence
F . y = Class (E,(o . x))
by A15, A22; verum