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) ) )
proof
deffunc H1( 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 = H1(i) ) ) from rng p c= Y
proof
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 = H1(x) by A1, A2;
x in dom the Enumeration of P by ;
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 ; :: thesis: verum
end;
then reconsider p = p as FinSequence of Y by FINSEQ_1:def 4;
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;
hence ( not P is empty implies 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) ) ) ) ; :: thesis: ( P is empty implies ex b1 being FinSequence of Y st b1 = <*> Y )
thus ( P is empty implies ex p being FinSequence of Y st p = <*> Y ) ; :: thesis: verum