set pr = product B;

set ca = ComAr O;

set ct = (ComAr O) -tuples_on (product B);

defpred S_{1}[ 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_{1}[x,y] )

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_{1}[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

take f ; :: thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds

( ( 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) ) ) ) )

thus dom f = (ComAr O) -tuples_on (product B) by A27; :: thesis: for p being Element of (product B) * st p in dom f holds

( ( 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) ) )

let p be Element of (product B) * ; :: thesis: ( p in dom f implies ( ( 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) ) ) )

assume p in dom f ; :: thesis: ( ( 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) ) )

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: verum

set ca = ComAr O;

set ct = (ComAr O) -tuples_on (product B);

defpred S

( ( 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

proof

consider f being Function such that
let x be object ; :: thesis: ( x in (ComAr O) -tuples_on (product B) implies ex y being object st

( y in product B & S_{1}[x,y] ) )

assume x in (ComAr O) -tuples_on (product B) ; :: thesis: ex y being object st

( y in product B & S_{1}[x,y] )

then consider w being Element of (product B) * such that

A2: x = w and

A3: len w = ComAr O ;

( y in product B & S_{1}[x,y] )
; :: thesis: verum

end;( y in product B & S

assume x in (ComAr O) -tuples_on (product B) ; :: thesis: ex y being object st

( y in product B & S

then consider w being Element of (product B) * 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 (product B) * st p = x holds

( ( 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) ) ) ) ) ) or ( dom w <> {} & ex y being Function st

( y in product B & ( for l being Element of (product B) * st l = x holds

( ( 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) ) ) ) ) ) )end;

hence
ex y being object st ( y in product B & ( for p being Element of (product B) * st p = x holds

( ( 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) ) ) ) ) ) or ( dom w <> {} & ex y being Function st

( y in product B & ( for l being Element of (product B) * st l = x holds

( ( 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) ) ) ) ) ) )

per cases
( dom w = {} or dom w <> {} )
;

end;

case A4:
dom w = {}
; :: thesis: ex y being Function st

( y in product B & ( for p being Element of (product B) * st p = x holds

( ( 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) ) ) ) )

( y in product B & ( for p being Element of (product B) * st p = x holds

( ( 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) ) ) ) )

A5:
for z being object st z in dom B holds

(O .. (EmptyMS J)) . z in B . z

( ( 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) ) ) ) )

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: for p being Element of (product B) * st p = x holds

( ( 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) ) )

let p be Element of (product B) * ; :: thesis: ( p = x implies ( ( 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) ) ) )

assume p = x ; :: thesis: ( ( 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) ) )

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: verum

end;(O .. (EmptyMS J)) . z in B . z

proof

take y = O .. (EmptyMS J); :: thesis: ( y in product B & ( for p being Element of (product B) * st p = x holds
let z be object ; :: thesis: ( z in dom B implies (O .. (EmptyMS J)) . z in B . z )

assume z in dom B ; :: thesis: (O .. (EmptyMS J)) . 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 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: verum

end;assume z in dom B ; :: thesis: (O .. (EmptyMS J)) . 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 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: verum

( ( 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) ) ) ) )

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: for p being Element of (product B) * st p = x holds

( ( 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) ) )

let p be Element of (product B) * ; :: thesis: ( p = x implies ( ( 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) ) ) )

assume p = x ; :: thesis: ( ( 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) ) )

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: verum

case
dom w <> {}
; :: thesis: ex y being Function st

( y in product B & ( for l being Element of (product B) * st l = x holds

( ( 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) ) ) ) )

( y in product B & ( for l being Element of (product B) * st l = x holds

( ( 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) ) ) ) )

then reconsider Z = dom w as non empty set ;

reconsider p = ~ (uncurry w) as ManySortedSet of [:J,Z:] ;

take y = O .. (curry p); :: thesis: ( y in product B & ( for l being Element of (product B) * st l = x holds

( ( 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) ) ) ) )

A8: for z being object st z in dom B holds

(O .. (curry p)) . z in B . z

.= dom B by PARTFUN1:def 2 ;

hence y in product B by A8, CARD_3:def 5; :: thesis: for l being Element of (product B) * st l = x holds

( ( 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) ) )

let l be Element of (product B) * ; :: thesis: ( l = x implies ( ( 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) ) ) )

assume l = x ; :: thesis: ( ( 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) ) )

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: verum

end;reconsider p = ~ (uncurry w) as ManySortedSet of [:J,Z:] ;

take y = O .. (curry p); :: thesis: ( y in product B & ( for l being Element of (product B) * st l = x holds

( ( 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) ) ) ) )

A8: for z being object st z in dom B holds

(O .. (curry p)) . z in B . z

proof

dom (O .. (curry p)) =
J
by PARTFUN1:def 2
let z be object ; :: thesis: ( z in dom B implies (O .. (curry p)) . z in B . z )

assume z in dom B ; :: thesis: (O .. (curry p)) . 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 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

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: verum

end;assume z in dom B ; :: thesis: (O .. (curry p)) . 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 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

proof

then reconsider g = g as FinSequence of B . j by FINSEQ_1:def 4;
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 (uncurry w) = [:(dom w),J:] & dom g = dom w ) by A13, FINSEQ_1:def 3, PARTFUN1:def 2;

then A16: [x,j] in dom (uncurry w) by A14, ZFMISC_1:87;

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 = (~ (uncurry w)) . (j,x) by A12, A14, A15;

then A21: y = (uncurry w) . (x,j) by A16, FUNCT_4:def 2;

( [a,b] `1 = a & [a,b] `2 = j ) by A17;

then A22: y = f . j by A16, A21, A17, A19, FUNCT_5:def 2;

A23: j = b by A17, XTUPLE_0:1;

A24: ( rng w c= product B & w . a in rng w ) by A18, FINSEQ_1:def 4, FUNCT_1:def 3;

then dom f = dom B by A19, CARD_3:9;

hence y in B . j by A19, A20, A23, A24, A22, CARD_3:9; :: thesis: verum

end;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 (uncurry w) = [:(dom w),J:] & dom g = dom w ) by A13, FINSEQ_1:def 3, PARTFUN1:def 2;

then A16: [x,j] in dom (uncurry w) by A14, ZFMISC_1:87;

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 = (~ (uncurry w)) . (j,x) by A12, A14, A15;

then A21: y = (uncurry w) . (x,j) by A16, FUNCT_4:def 2;

( [a,b] `1 = a & [a,b] `2 = j ) by A17;

then A22: y = f . j by A16, A21, A17, A19, FUNCT_5:def 2;

A23: j = b by A17, XTUPLE_0:1;

A24: ( rng w c= product B & w . a in rng w ) by A18, FINSEQ_1:def 4, FUNCT_1:def 3;

then dom f = dom B by A19, CARD_3:9;

hence y in B . j by A19, A20, A23, A24, A22, CARD_3:9; :: thesis: verum

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: verum

.= dom B by PARTFUN1:def 2 ;

hence y in product B by A8, CARD_3:def 5; :: thesis: for l being Element of (product B) * st l = x holds

( ( 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) ) )

let l be Element of (product B) * ; :: thesis: ( l = x implies ( ( 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) ) ) )

assume l = x ; :: thesis: ( ( 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) ) )

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: verum

( y in product B & S

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

(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

proof

f is quasi_total
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 (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: verum

end;assume A30: ( x in dom f & y in dom f ) ; :: thesis: len x = len y

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: verum

proof

then reconsider f = f as non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) by A27, A29;
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 (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: verum

end;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 (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: verum

take f ; :: thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds

( ( 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) ) ) ) )

thus dom f = (ComAr O) -tuples_on (product B) by A27; :: thesis: for p being Element of (product B) * st p in dom f holds

( ( 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) ) )

let p be Element of (product B) * ; :: thesis: ( p in dom f implies ( ( 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) ) ) )

assume p in dom f ; :: thesis: ( ( 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) ) )

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: verum