set ar = (arity f1) -tuples_on [:A,B:];

set ab = { s where s is Element of [:A,B:] * : len s = arity f1 } ;

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

y in [:A,B:]_{1}[x,y] & S_{1}[x,z] holds

y = z

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

A18: for x being object st x in dom f holds

S_{1}[x,f . x]
from PARTFUN1:sch 2(A5, A12);

A19: dom f = (arity f1) -tuples_on [:A,B:]

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

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

set ab = { s where s is Element of [:A,B:] * : len s = arity f1 } ;

defpred S

$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

y in [:A,B:]

proof

A12:
for x, y, z being object st x in (arity f1) -tuples_on [:A,B:] & S
let x, y be object ; :: thesis: ( x in (arity f1) -tuples_on [:A,B:] & S_{1}[x,y] implies y in [:A,B:] )

assume that

A6: x in (arity f1) -tuples_on [:A,B:] and

A7: S_{1}[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;assume that

A6: x in (arity f1) -tuples_on [:A,B:] and

A7: S

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

y = z

proof

consider f being PartFunc of ((arity f1) -tuples_on [:A,B:]),[:A,B:] such that
let x, y, z be object ; :: thesis: ( x in (arity f1) -tuples_on [:A,B:] & S_{1}[x,y] & S_{1}[x,z] implies y = z )

assume that

A13: x in (arity f1) -tuples_on [:A,B:] and

A14: S_{1}[x,y]
and

A15: S_{1}[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;assume that

A13: x in (arity f1) -tuples_on [:A,B:] and

A14: S

A15: S

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

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

A18: for x being object st x in dom f holds

S

A19: dom f = (arity f1) -tuples_on [:A,B:]

proof

(arity f1) -tuples_on [:A,B:] in { (i -tuples_on [:A,B:]) where i is Nat : verum }
;
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 ;

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

hence
x in dom f
by A17, A20; :: thesis: verumfor 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;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

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

f is homogeneous
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;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

proof

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

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