ex p being FinSequence of Y st

( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) )

( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) ) ) ; :: thesis: ( P is empty implies ex b_{1} being FinSequence of Y st b_{1} = <*> Y )

thus ( P is empty implies ex p being FinSequence of Y st p = <*> Y ) ; :: thesis: verum

( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) )

proof

hence
( not P is empty implies ex p being FinSequence of Y st
deffunc H_{1}( Nat) -> set = M0 . ( the Enumeration of P . $1);

consider p being FinSequence such that

A1: ( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = H_{1}(i) ) )
from FINSEQ_1:sch 2();

rng p c= Y

take p ; :: thesis: ( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) )

thus ( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) ) by A1; :: thesis: verum

end;consider p being FinSequence such that

A1: ( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = H

rng p c= Y

proof

then reconsider p = p as FinSequence of Y by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in Y )

assume y in rng p ; :: thesis: y in Y

then consider x being object such that

A2: ( x in dom p & y = p . x ) by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A2;

A3: y = H_{1}(x)
by A1, A2;

x in dom the Enumeration of P by A2, FINSEQ_3:29, A1;

then the Enumeration of P . x in rng the Enumeration of P by FUNCT_1:3;

then the Enumeration of P . x in P by RLAFFIN3:def 1;

hence y in Y by A3, FUNCT_2:5; :: thesis: verum

end;assume y in rng p ; :: thesis: y in Y

then consider x being object such that

A2: ( x in dom p & y = p . x ) by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A2;

A3: y = H

x in dom the Enumeration of P by A2, FINSEQ_3:29, A1;

then the Enumeration of P . x in rng the Enumeration of P by FUNCT_1:3;

then the Enumeration of P . x in P by RLAFFIN3:def 1;

hence y in Y by A3, FUNCT_2:5; :: thesis: verum

take p ; :: thesis: ( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) )

thus ( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) ) by A1; :: thesis: verum

( len p = len the Enumeration of P & ( for i being Nat st i in dom p holds

p . i = M0 . ( the Enumeration of P . i) ) ) ) ; :: thesis: ( P is empty implies ex b

thus ( P is empty implies ex p being FinSequence of Y st p = <*> Y ) ; :: thesis: verum