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

proof

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;

A5: dom (o | ((arity o) -tuples_on A)) = (dom o) /\ ((arity o) -tuples_on A) by RELAT_1:61
.= ((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

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;

(arity o) -tuples_on A in { (i -tuples_on A) where i is Nat : 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

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;

oa is quasi_total

proof

let x1 be FinSequence of A; :: according to MARGREL1:def 22 :: thesis: for b₁ being FinSequence of A holds
( not len x1 = len b₁ or not x1 in dom oa or b₁ 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;

hence o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A by A5, A11; :: thesis: verum