let g be ConwayGame; :: thesis: ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g )
take f = <*g*>; :: thesis: ( f . 1 = g & f . (len f) = g )
len f = 1 by FINSEQ_1:40;
hence ( f . 1 = g & f . (len f) = g ) ; :: thesis: verum