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

let x be object ; :: thesis:
assume x in (ComAr O) -tuples_on (product B) ; :: thesis:
then consider w being Element of (product B) * such that
A2: x = w and
A3: len w = ComAr O ;

let z be object ; :: thesis:
assume z in dom B ; :: thesis:
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 A3, Def19;
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 .. (EmptyMS J)) . z = (O . j) . ((EmptyMS J) . j) by Def18
.= (O . j) . ({} (B . j)) ;
hence (O .. (EmptyMS J)) . z in B . z by A7, A6; :: thesis:

end;

take y = O .. (EmptyMS J); :: thesis:
dom (O .. (EmptyMS J)) = J by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
hence y in product B by A5, CARD_3:def 5; :: thesis:
let p be Element of (product B) * ; :: thesis:
assume p = x ; :: thesis:
hence ( ( dom p = {} implies y = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
y = O .. (curry w) ) ) by A2, A4; :: thesis:

end;

then reconsider Z = dom w as non empty set ;
reconsider p = ~ (uncurry w) as ManySortedSet of [:J,Z:] ;
take y = O .. (curry p); :: thesis:
A8: for z being object st z in dom B holds
(O .. (curry p)) . z in B . z

let z be object ; :: thesis:
assume z in dom B ; :: thesis:
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 A9, FUNCT_5:9;
then A13: dom g = proj2 [:(J /\ {j}),(Z /\ Z):] by A9, A11, ZFMISC_1:100
.= 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

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) = (ComAr O) -tuples_on (B . j) by MARGREL1:22
.= { s where s is Element of (B . j) * : len s = ComAr O } ;
len g = len w by A13, FINSEQ_1:def 3;
then g in dom (O . j) by A3, A25;
then A26: (O . j) . g in rng (O . j) by FUNCT_1:def 3;
( (O .. (curry p)) . z = (O . j) . ((curry p) . j) & rng (O . j) c= B . j ) by Def18, RELAT_1:def 19;
hence (O .. (curry p)) . z in B . z by A10, A26; :: thesis:

end;

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

end;

end;

consider f being Function such that
A27: ( dom f = (ComAr O) -tuples_on (product B) & rng f c= product B & ( for x being object st x in (ComAr O) -tuples_on (product B) holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(A1);
(ComAr O) -tuples_on (product B) in { (n -tuples_on (product B)) where n is Nat : verum } ;
then A28: (ComAr O) -tuples_on (product B) c= union { (m -tuples_on (product B)) where m is Nat : verum } by ZFMISC_1:74;
then dom f c= (product B) * by A27, FINSEQ_2:108;
then reconsider f = f as PartFunc of ((product B) *),(product B) by A27, RELSET_1:4;
A29: f is homogeneous

let x, y be FinSequence; :: according to MARGREL1:def 1,MARGREL1:def 21 :: thesis:
assume A30: ( x in dom f & y in dom f ) ; :: thesis:
then reconsider x1 = x, y1 = y as Element of (product B) * by A27, A28, FINSEQ_2:108;
( ex w being Element of (product B) * st
( x1 = w & len w = ComAr O ) & ex w being Element of (product B) * st
( y1 = w & len w = ComAr O ) ) by A27, A30;
hence len x = len y ; :: thesis:

end;

let x, y be FinSequence of product B; :: according to MARGREL1:def 22 :: thesis:
assume that
A31: len x = len y and
A32: x in dom f ; :: thesis:
reconsider x1 = x, y1 = y as Element of (product B) * by FINSEQ_1:def 11;
ex w being Element of (product B) * st
( x1 = w & len w = ComAr O ) by A27, A32;
then y1 in { q where q is Element of (product B) * : len q = ComAr O } by A31;
hence y in proj1 f by A27; :: thesis:

end;

then reconsider f = f as non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) by A27, A29;
take f ; :: thesis:
thus dom f = (ComAr O) -tuples_on (product B) by A27; :: thesis:
let p be Element of (product B) * ; :: thesis:
assume p in dom f ; :: thesis:
hence ( ( dom p = {} implies f . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
f . p = O .. (curry w) ) ) by A27; :: thesis: