set pr = product B;
set ca = ComAr O;
set ct = () -tuples_on ();
defpred S1[ object , object ] means for p being Element of () * st p = \$1 holds
( ( dom p = {} implies \$2 = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
\$2 = O .. () ) );
set aa = { q where q is Element of () * : len q = ComAr O } ;
A1: for x being object st x in () -tuples_on () holds
ex y being object st
( y in product B & S1[x,y] )
proof
let x be object ; :: thesis: ( x in () -tuples_on () implies ex y being object st
( y in product B & S1[x,y] ) )

assume x in () -tuples_on () ; :: thesis: ex y being object st
( y in product B & S1[x,y] )

then consider w being Element of () * such that
A2: x = w and
A3: len w = ComAr O ;
now :: thesis: ( ( dom w = {} & ex y being Function st
( y in product B & ( for p being Element of () * st p = x holds
( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) ) ) ) ) or ( dom w <> {} & ex y being Function st
( y in product B & ( for l being Element of () * st l = x holds
( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) ) ) ) ) )
per cases ( dom w = {} or dom w <> {} ) ;
case A4: dom w = {} ; :: thesis: ex y being Function st
( y in product B & ( for p being Element of () * st p = x holds
( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) ) ) )

A5: for z being object st z in dom B holds
(O .. ()) . z in B . z
proof
let z be object ; :: thesis: ( z in dom B implies (O .. ()) . z in B . z )
assume z in dom B ; :: thesis: (O .. ()) . z in B . z
then reconsider j = z as Element of J by PARTFUN1:def 2;
A6: rng (O . j) c= B . j by RELAT_1:def 19;
w = {} by A4;
then arity (O . j) = 0 by ;
then dom (O . j) = 0 -tuples_on (B . j) by MARGREL1:22
.= {(<*> (B . j))} by FINSEQ_2:94 ;
then {} (B . j) in dom (O . j) by TARSKI:def 1;
then A7: (O . j) . ({} (B . j)) in rng (O . j) by FUNCT_1:def 3;
(O .. ()) . z = (O . j) . (() . j) by Def18
.= (O . j) . ({} (B . j)) ;
hence (O .. ()) . z in B . z by A7, A6; :: thesis: verum
end;
take y = O .. (); :: thesis: ( y in product B & ( for p being Element of () * st p = x holds
( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) ) ) )

dom (O .. ()) = J by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
hence y in product B by ; :: thesis: for p being Element of () * st p = x holds
( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) )

let p be Element of () * ; :: thesis: ( p = x implies ( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) ) )

assume p = x ; :: thesis: ( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) )

hence ( ( dom p = {} implies y = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
y = O .. () ) ) by A2, A4; :: thesis: verum
end;
case dom w <> {} ; :: thesis: ex y being Function st
( y in product B & ( for l being Element of () * st l = x holds
( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) ) ) )

then reconsider Z = dom w as non empty set ;
reconsider p = ~ () as ManySortedSet of [:J,Z:] ;
take y = O .. (); :: thesis: ( y in product B & ( for l being Element of () * st l = x holds
( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) ) ) )

A8: for z being object st z in dom B holds
(O .. ()) . z in B . z
proof
let z be object ; :: thesis: ( z in dom B implies (O .. ()) . z in B . z )
assume z in dom B ; :: thesis: (O .. ()) . z in B . z
then reconsider j = z as Element of J by PARTFUN1:def 2;
A9: dom p = [:J,Z:] by PARTFUN1:def 2;
then proj1 (dom p) = J by FUNCT_5:9;
then consider g being Function such that
A10: (curry p) . j = g and
A11: dom g = proj2 ((dom p) /\ [:{j},(proj2 (dom p)):]) and
A12: for y being object st y in dom g holds
g . y = p . (j,y) by FUNCT_5:def 1;
proj2 (dom p) = Z by ;
then A13: dom g = proj2 [:(J /\ {j}),(Z /\ Z):] by
.= proj2 [:{j},Z:] by ZFMISC_1:46
.= dom w by FUNCT_5:9
.= Seg (len w) by FINSEQ_1:def 3 ;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
rng g c= B . j
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in B . j )
assume y in rng g ; :: thesis: y in B . j
then consider x being object such that
A14: x in dom g and
A15: g . x = y by FUNCT_1:def 3;
( dom () = [:(dom w),J:] & dom g = dom w ) by ;
then A16: [x,j] in dom () by ;
then consider a being object , f being Function, b being object such that
A17: [x,j] = [a,b] and
A18: a in dom w and
A19: f = w . a and
A20: b in dom f by FUNCT_5:def 2;
y = (~ ()) . (j,x) by ;
then A21: y = () . (x,j) by ;
( [a,b] `1 = a & [a,b] `2 = j ) by A17;
then A22: y = f . j by ;
A23: j = b by ;
A24: ( rng w c= product B & w . a in rng w ) by ;
then dom f = dom B by ;
hence y in B . j by ; :: thesis: verum
end;
then reconsider g = g as FinSequence of B . j by FINSEQ_1:def 4;
reconsider g = g as Element of (B . j) * by FINSEQ_1:def 11;
arity (O . j) = ComAr O by Def19;
then A25: dom (O . j) = () -tuples_on (B . j) by MARGREL1:22
.= { s where s is Element of (B . j) * : len s = ComAr O } ;
len g = len w by ;
then g in dom (O . j) by ;
then A26: (O . j) . g in rng (O . j) by FUNCT_1:def 3;
( (O .. ()) . z = (O . j) . (() . j) & rng (O . j) c= B . j ) by ;
hence (O .. ()) . z in B . z by ; :: thesis: verum
end;
dom (O .. ()) = J by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
hence y in product B by ; :: thesis: for l being Element of () * st l = x holds
( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) )

let l be Element of () * ; :: thesis: ( l = x implies ( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) ) )

assume l = x ; :: thesis: ( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) )

hence ( ( dom l = {} implies y = O .. () ) & ( dom l <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ () holds
y = O .. () ) ) by A2; :: thesis: verum
end;
end;
end;
hence ex y being object st
( y in product B & S1[x,y] ) ; :: thesis: verum
end;
consider f being Function such that
A27: ( dom f = () -tuples_on () & rng f c= product B & ( for x being object st x in () -tuples_on () holds
S1[x,f . x] ) ) from (ComAr O) -tuples_on () in { (n -tuples_on ()) where n is Nat : verum } ;
then A28: (ComAr O) -tuples_on () c= union { (m -tuples_on ()) where m is Nat : verum } by ZFMISC_1:74;
then dom f c= () * by ;
then reconsider f = f as PartFunc of (() *),() by ;
A29: f is homogeneous
proof
let x, y be FinSequence; :: according to MARGREL1:def 1,MARGREL1:def 21 :: thesis: ( not x in proj1 f or not y in proj1 f or len x = len y )
assume A30: ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then reconsider x1 = x, y1 = y as Element of () * by ;
( ex w being Element of () * st
( x1 = w & len w = ComAr O ) & ex w being Element of () * st
( y1 = w & len w = ComAr O ) ) by ;
hence len x = len y ; :: thesis: verum
end;
f is quasi_total
proof
let x, y be FinSequence of product B; :: according to MARGREL1:def 22 :: thesis: ( not len x = len y or not x in proj1 f or y in proj1 f )
assume that
A31: len x = len y and
A32: x in dom f ; :: thesis: y in proj1 f
reconsider x1 = x, y1 = y as Element of () * by FINSEQ_1:def 11;
ex w being Element of () * st
( x1 = w & len w = ComAr O ) by ;
then y1 in { q where q is Element of () * : len q = ComAr O } by A31;
hence y in proj1 f by A27; :: thesis: verum
end;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of (() *),() by ;
take f ; :: thesis: ( dom f = () -tuples_on () & ( for p being Element of () * st p in dom f holds
( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) ) ) )

thus dom f = () -tuples_on () by A27; :: thesis: for p being Element of () * st p in dom f holds
( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) )

let p be Element of () * ; :: thesis: ( p in dom f implies ( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) ) )

assume p in dom f ; :: thesis: ( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) )

hence ( ( dom p = {} implies f . p = O .. () ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ () holds
f . p = O .. () ) ) by A27; :: thesis: verum