set ar = (arity f1) -tuples_on [:A,B:];
set ab = { s where s is Element of [:A,B:] * : len s = arity f1 } ;
defpred S₁[ object , object ] means for h being FinSequence of [:A,B:] st $1 = h holds
$2 = [(f1 . (pr1 h)),(f2 . (pr2 h))];
A2: dom f2 = (arity f2) -tuples_on B by MARGREL1:22;
A3: ( rng f1 c= A & rng f2 c= B ) by RELAT_1:def 19;
A4: dom f1 = (arity f1) -tuples_on A by MARGREL1:22;
A5: for x, y being object st x in (arity f1) -tuples_on [:A,B:] & S₁[x,y] holds
y in [:A,B:]

proof

let x, y be object ; :: thesis: ( x in (arity f1) -tuples_on [:A,B:] & S₁[x,y] implies y in [:A,B:] )
assume that
A6: x in (arity f1) -tuples_on [:A,B:] and
A7: S₁[x,y] ; :: thesis: y in [:A,B:]
consider s being Element of [:A,B:] * such that
A8: x = s and
A9: len s = arity f1 by A6;
reconsider s1 = pr1 s as Element of A * by FINSEQ_1:def 11;
len (pr1 s) = len s by Def1;
then s1 in { s3 where s3 is Element of A * : len s3 = arity f1 } by A9;
then A10: f1 . s1 in rng f1 by A4, FUNCT_1:def 3;
reconsider s2 = pr2 s as Element of B * by FINSEQ_1:def 11;
len (pr2 s) = len s by Def2;
then s2 in { s3 where s3 is Element of B * : len s3 = arity f2 } by A1, A9;
then A11: f2 . s2 in rng f2 by A2, FUNCT_1:def 3;
y = [(f1 . (pr1 s)),(f2 . (pr2 s))] by A7, A8;
hence y in [:A,B:] by A3, A10, A11, ZFMISC_1:87; :: thesis: verum

end;

A12: for x, y, z being object st x in (arity f1) -tuples_on [:A,B:] & S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( x in (arity f1) -tuples_on [:A,B:] & S₁[x,y] & S₁[x,z] implies y = z )
assume that
A13: x in (arity f1) -tuples_on [:A,B:] and
A14: S₁[x,y] and
A15: S₁[x,z] ; :: thesis: y = z
consider s being Element of [:A,B:] * such that
A16: x = s and
len s = arity f1 by A13;
y = [(f1 . (pr1 s)),(f2 . (pr2 s))] by A14, A16;
hence y = z by A15, A16; :: thesis: verum

end;

consider f being PartFunc of ((arity f1) -tuples_on [:A,B:]),[:A,B:] such that
A17: for x being object holds
( x in dom f iff ( x in (arity f1) -tuples_on [:A,B:] & ex y being object st S₁[x,y] ) ) and
A18: for x being object st x in dom f holds
S₁[x,f . x] from PARTFUN1:sch 2(A5, A12);
A19: dom f = (arity f1) -tuples_on [:A,B:]

proof

thus dom f c= (arity f1) -tuples_on [:A,B:] by A17; :: according to XBOOLE_0:def 10 :: thesis: (arity f1) -tuples_on [:A,B:] c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (arity f1) -tuples_on [:A,B:] or x in dom f )
assume A20: x in (arity f1) -tuples_on [:A,B:] ; :: thesis: x in dom f
then consider s being Element of [:A,B:] * such that
A21: x = s and
len s = arity f1 ;

now :: thesis: ex y being object st
for h being FinSequence of [:A,B:] st h = x holds
y = [(f1 . (pr1 h)),(f2 . (pr2 h))]

take y = [(f1 . (pr1 s)),(f2 . (pr2 s))]; :: thesis: for h being FinSequence of [:A,B:] st h = x holds
y = [(f1 . (pr1 h)),(f2 . (pr2 h))]
let h be FinSequence of [:A,B:]; :: thesis: ( h = x implies y = [(f1 . (pr1 h)),(f2 . (pr2 h))] )
assume h = x ; :: thesis: y = [(f1 . (pr1 h)),(f2 . (pr2 h))]
hence y = [(f1 . (pr1 h)),(f2 . (pr2 h))] by A21; :: thesis: verum

end;

hence x in dom f by A17, A20; :: thesis: verum

end;

(arity f1) -tuples_on [:A,B:] in { (i -tuples_on [:A,B:]) where i is Nat : verum } ;
then (arity f1) -tuples_on [:A,B:] c= union { (i -tuples_on [:A,B:]) where i is Nat : verum } by ZFMISC_1:74;
then (arity f1) -tuples_on [:A,B:] c= [:A,B:] * by FINSEQ_2:108;
then reconsider f = f as PartFunc of ([:A,B:] *),[:A,B:] by RELSET_1:7;
A22: f is quasi_total

proof

let x, y be FinSequence of [:A,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
A23: len x = len y and
A24: x in dom f ; :: thesis: y in proj1 f
reconsider y9 = y as Element of [:A,B:] * by FINSEQ_1:def 11;
ex s1 being Element of [:A,B:] * st
( s1 = x & len s1 = arity f1 ) by A19, A24;
then y9 in { s where s is Element of [:A,B:] * : len s = arity f1 } by A23;
hence y in proj1 f by A19; :: thesis: verum

end;

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 ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then ( ex s1 being Element of [:A,B:] * st
( s1 = x & len s1 = arity f1 ) & ex s2 being Element of [:A,B:] * st
( s2 = y & len s2 = arity f1 ) ) by A19;
hence len x = len y ; :: thesis: verum

end;

then reconsider f = f as non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] by A19, A22;
take f ; :: thesis: ( dom f = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom f holds
f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )
thus dom f = (arity f1) -tuples_on [:A,B:] by A19; :: thesis: for h being FinSequence of [:A,B:] st h in dom f holds
f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))]
let h be FinSequence of [:A,B:]; :: thesis: ( h in dom f implies f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] )
assume h in dom f ; :: thesis: f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))]
hence f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] by A18; :: thesis: verum