deffunc H_{1}( object ) -> set = rng (F_{1}() . $1);

consider p being XFinSequence such that

A1: len p = len F_{1}()
and

A2: for k being Nat st k in len F_{1}() holds

p . k = H_{1}(k)
from AFINSQ_1:sch 2();

for X being set st X in rng p holds

X is finite

{ ((F_{1}() . i) . j) where i, j is Nat : P_{1}[i,j] } c= {0} \/ (union (rng p))
_{1}() . i) . j) where i, j is Nat : P_{1}[i,j] } is finite
by A5; :: thesis: verum

consider p being XFinSequence such that

A1: len p = len F

A2: for k being Nat st k in len F

p . k = H

for X being set st X in rng p holds

X is finite

proof

then A5:
union (rng p) is finite
by FINSET_1:7;
let X be set ; :: thesis: ( X in rng p implies X is finite )

assume A3: X in rng p ; :: thesis: X is finite

consider x being object such that

A4: ( x in dom p & p . x = X ) by A3, FUNCT_1:def 3;

p . x = H_{1}(x)
by A1, A2, A4;

hence X is finite by A4; :: thesis: verum

end;assume A3: X in rng p ; :: thesis: X is finite

consider x being object such that

A4: ( x in dom p & p . x = X ) by A3, FUNCT_1:def 3;

p . x = H

hence X is finite by A4; :: thesis: verum

{ ((F

proof

hence
{ ((F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((F_{1}() . i) . j) where i, j is Nat : P_{1}[i,j] } or x in {0} \/ (union (rng p)) )

assume x in { ((F_{1}() . i) . j) where i, j is Nat : P_{1}[i,j] }
; :: thesis: x in {0} \/ (union (rng p))

then consider i, j being Nat such that

A6: ( x = (F_{1}() . i) . j & P_{1}[i,j] )
;

end;assume x in { ((F

then consider i, j being Nat such that

A6: ( x = (F

now :: thesis: ( not x in {0} implies x in union (rng p) )

hence
x in {0} \/ (union (rng p))
by XBOOLE_0:def 3; :: thesis: verumassume
not x in {0}
; :: thesis: x in union (rng p)

then A7: x <> 0 by TARSKI:def 1;

then j in dom (F_{1}() . i)
by A6, FUNCT_1:def 2;

then A8: (F_{1}() . i) . j in rng (F_{1}() . i)
by FUNCT_1:def 3;

F_{1}() . i <> {}
by A6, A7;

then i in dom F_{1}()
by FUNCT_1:def 2;

then ( F_{1}() . i in rng F_{1}() & p . i = H_{1}(i) & p . i in rng p )
by A1, A2, FUNCT_1:def 3;

hence x in union (rng p) by A8, A6, TARSKI:def 4; :: thesis: verum

end;then A7: x <> 0 by TARSKI:def 1;

then j in dom (F

then A8: (F

F

then i in dom F

then ( F

hence x in union (rng p) by A8, A6, TARSKI:def 4; :: thesis: verum