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:57;
hence ( f . 1 = g & f . (len f) = g ) by FINSEQ_1:57; :: thesis: verum