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

proof

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

end;

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

proof

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

end;

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

proof

thus dom f c= (arity f1) -tuples_on [:A,B:] :: according to XBOOLE_0:def 10 :: thesis: (arity f1) -tuples_on [:A,B:] c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in (arity f1) -tuples_on [:A,B:] )
assume x in dom f ; :: thesis: x in (arity f1) -tuples_on [:A,B:]
hence x in (arity f1) -tuples_on [:A,B:] by A15; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (arity f1) -tuples_on [:A,B:] or x in dom f )
assume A18: x in (arity f1) -tuples_on [:A,B:] ; :: thesis: x in dom f
then consider s being Element of [:A,B:] * such that
A19: ( x = s & len s = arity f1 ) ;

now

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 A19; :: thesis: verum

end;

hence x in dom f by A15, A18; :: thesis: verum

end;

(arity f1) -tuples_on [:A,B:] in { (i -tuples_on [:A,B:]) where i is Element of NAT : verum } ;
then (arity f1) -tuples_on [:A,B:] c= union { (i -tuples_on [:A,B:]) where i is Element of NAT : verum } by ZFMISC_1:92;
then (arity f1) -tuples_on [:A,B:] c= [:A,B:] * by FINSEQ_2:128;
then reconsider f = f as PartFunc of ([:A,B:] * ),[:A,B:] by RELSET_1:17;
A20: f is homogeneous

proof

let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in proj1 f or not y in proj1 f or len x = len y )
assume A21: ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then consider s1 being Element of [:A,B:] * such that
A22: ( s1 = x & len s1 = arity f1 ) by A17;
consider s2 being Element of [:A,B:] * such that
A23: ( s2 = y & len s2 = arity f1 ) by A17, A21;
thus len x = len y by A22, A23; :: thesis: verum

end;

f is quasi_total

proof

let x, y be FinSequence of [:A,B:]; :: according to UNIALG_1:def 2 :: thesis: ( not len x = len y or not x in proj1 f or y in proj1 f )
assume A24: ( len x = len y & x in dom f ) ; :: thesis: y in proj1 f
then consider s1 being Element of [:A,B:] * such that
A25: ( s1 = x & len s1 = arity f1 ) by A17;
reconsider y' = y as Element of [:A,B:] * by FINSEQ_1:def 11;
y' in { s where s is Element of [:A,B:] * : len s = arity f1 } by A24, A25;
hence y in proj1 f by A17; :: thesis: verum

end;

then reconsider f = f as non empty homogeneous quasi_total PartFunc of ([:A,B:] * ),[:A,B:] by A17, A20;
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 A17; :: 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 A16; :: thesis: verum