let alpha be Ordinal; :: thesis: for f being ConwayGameChain st f . (len f) in ConwayDay alpha holds
f . 1 in ConwayDay alpha
let f be ConwayGameChain; :: thesis: ( f . (len f) in ConwayDay alpha implies f . 1 in ConwayDay alpha )
assume A1: f . (len f) in ConwayDay alpha ; :: thesis: f . 1 in ConwayDay alpha
reconsider n = 1 as Element of dom f by FINSEQ_5:6;
reconsider m = len f as Element of dom f by FINSEQ_5:6;
n <= m by NAT_1:14;
then ( ConwayRank (f . n) c= ConwayRank (f . m) & ConwayRank (f . m) c= alpha ) by Th22, A1, Th12;
then ConwayRank (f . n) c= alpha ;
hence f . 1 in ConwayDay alpha by Th12; :: thesis: verum