A2:
(arity o) -tuples_on A c= (arity o) -tuples_on the carrier of U0

.= ((arity o) -tuples_on the carrier of U0) /\ ((arity o) -tuples_on A) by MARGREL1:22

.= (arity o) -tuples_on A by A2, XBOOLE_1:28 ;

A6: rng (o | ((arity o) -tuples_on A)) c= A

then (arity o) -tuples_on A c= union { (i -tuples_on A) where i is Nat : verum } by ZFMISC_1:74;

then dom (o | ((arity o) -tuples_on A)) c= A * by A5, FINSEQ_2:108;

then reconsider oa = o | ((arity o) -tuples_on A) as PartFunc of (A *),A by A6, RELSET_1:4;

A11: oa is homogeneous

proof

A5: dom (o | ((arity o) -tuples_on A)) =
(dom o) /\ ((arity o) -tuples_on A)
by RELAT_1:61
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (arity o) -tuples_on A or x in (arity o) -tuples_on the carrier of U0 )

assume x in (arity o) -tuples_on A ; :: thesis: x in (arity o) -tuples_on the carrier of U0

then x in { s where s is Element of A * : len s = arity o } by FINSEQ_2:def 4;

then consider s being Element of A * such that

A3: x = s and

A4: len s = arity o ;

rng s c= A by FINSEQ_1:def 4;

then rng s c= the carrier of U0 by XBOOLE_1:1;

then reconsider s = s as FinSequence of the carrier of U0 by FINSEQ_1:def 4;

reconsider s = s as Element of the carrier of U0 * by FINSEQ_1:def 11;

x = s by A3;

then x in { s1 where s1 is Element of the carrier of U0 * : len s1 = arity o } by A4;

hence x in (arity o) -tuples_on the carrier of U0 by FINSEQ_2:def 4; :: thesis: verum

end;assume x in (arity o) -tuples_on A ; :: thesis: x in (arity o) -tuples_on the carrier of U0

then x in { s where s is Element of A * : len s = arity o } by FINSEQ_2:def 4;

then consider s being Element of A * such that

A3: x = s and

A4: len s = arity o ;

rng s c= A by FINSEQ_1:def 4;

then rng s c= the carrier of U0 by XBOOLE_1:1;

then reconsider s = s as FinSequence of the carrier of U0 by FINSEQ_1:def 4;

reconsider s = s as Element of the carrier of U0 * by FINSEQ_1:def 11;

x = s by A3;

then x in { s1 where s1 is Element of the carrier of U0 * : len s1 = arity o } by A4;

hence x in (arity o) -tuples_on the carrier of U0 by FINSEQ_2:def 4; :: thesis: verum

.= ((arity o) -tuples_on the carrier of U0) /\ ((arity o) -tuples_on A) by MARGREL1:22

.= (arity o) -tuples_on A by A2, XBOOLE_1:28 ;

A6: rng (o | ((arity o) -tuples_on A)) c= A

proof

(arity o) -tuples_on A in { (i -tuples_on A) where i is Nat : verum }
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (o | ((arity o) -tuples_on A)) or x in A )

assume x in rng (o | ((arity o) -tuples_on A)) ; :: thesis: x in A

then consider y being object such that

A7: y in dom (o | ((arity o) -tuples_on A)) and

A8: x = (o | ((arity o) -tuples_on A)) . y by FUNCT_1:def 3;

y in { s where s is Element of A * : len s = arity o } by A5, A7, FINSEQ_2:def 4;

then consider s being Element of A * such that

A9: y = s and

A10: len s = arity o ;

(o | ((arity o) -tuples_on A)) . s = o . s by A7, A9, FUNCT_1:47;

hence x in A by A1, A8, A9, A10; :: thesis: verum

end;assume x in rng (o | ((arity o) -tuples_on A)) ; :: thesis: x in A

then consider y being object such that

A7: y in dom (o | ((arity o) -tuples_on A)) and

A8: x = (o | ((arity o) -tuples_on A)) . y by FUNCT_1:def 3;

y in { s where s is Element of A * : len s = arity o } by A5, A7, FINSEQ_2:def 4;

then consider s being Element of A * such that

A9: y = s and

A10: len s = arity o ;

(o | ((arity o) -tuples_on A)) . s = o . s by A7, A9, FUNCT_1:47;

hence x in A by A1, A8, A9, A10; :: thesis: verum

then (arity o) -tuples_on A c= union { (i -tuples_on A) where i is Nat : verum } by ZFMISC_1:74;

then dom (o | ((arity o) -tuples_on A)) c= A * by A5, FINSEQ_2:108;

then reconsider oa = o | ((arity o) -tuples_on A) as PartFunc of (A *),A by A6, RELSET_1:4;

A11: oa is homogeneous

proof

oa is quasi_total
let x1, y1 be FinSequence; :: according to MARGREL1:def 1,MARGREL1:def 21 :: thesis: ( not x1 in dom oa or not y1 in dom oa or len x1 = len y1 )

assume that

A12: x1 in dom oa and

A13: y1 in dom oa ; :: thesis: len x1 = len y1

y1 in { s1 where s1 is Element of A * : len s1 = arity o } by A5, A13, FINSEQ_2:def 4;

then A14: ex s1 being Element of A * st

( y1 = s1 & len s1 = arity o ) ;

x1 in { s where s is Element of A * : len s = arity o } by A5, A12, FINSEQ_2:def 4;

then ex s being Element of A * st

( x1 = s & len s = arity o ) ;

hence len x1 = len y1 by A14; :: thesis: verum

end;assume that

A12: x1 in dom oa and

A13: y1 in dom oa ; :: thesis: len x1 = len y1

y1 in { s1 where s1 is Element of A * : len s1 = arity o } by A5, A13, FINSEQ_2:def 4;

then A14: ex s1 being Element of A * st

( y1 = s1 & len s1 = arity o ) ;

x1 in { s where s is Element of A * : len s = arity o } by A5, A12, FINSEQ_2:def 4;

then ex s being Element of A * st

( x1 = s & len s = arity o ) ;

hence len x1 = len y1 by A14; :: thesis: verum

proof

hence
o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A
by A5, A11; :: thesis: verum
let x1 be FinSequence of A; :: according to MARGREL1:def 22 :: thesis: for b_{1} being FinSequence of A holds

( not len x1 = len b_{1} or not x1 in dom oa or b_{1} in dom oa )

let y1 be FinSequence of A; :: thesis: ( not len x1 = len y1 or not x1 in dom oa or y1 in dom oa )

assume that

A15: len x1 = len y1 and

A16: x1 in dom oa ; :: thesis: y1 in dom oa

x1 in { s where s is Element of A * : len s = arity o } by A5, A16, FINSEQ_2:def 4;

then ex s being Element of A * st

( x1 = s & len s = arity o ) ;

then y1 is Element of (arity o) -tuples_on A by A15, FINSEQ_2:92;

hence y1 in dom oa by A5; :: thesis: verum

end;( not len x1 = len b

let y1 be FinSequence of A; :: thesis: ( not len x1 = len y1 or not x1 in dom oa or y1 in dom oa )

assume that

A15: len x1 = len y1 and

A16: x1 in dom oa ; :: thesis: y1 in dom oa

x1 in { s where s is Element of A * : len s = arity o } by A5, A16, FINSEQ_2:def 4;

then ex s being Element of A * st

( x1 = s & len s = arity o ) ;

then y1 is Element of (arity o) -tuples_on A by A15, FINSEQ_2:92;

hence y1 in dom oa by A5; :: thesis: verum