for f1, f2 being ConwayGameChain st ex g being ConwayGame st
( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) holds
f1 ^ f2 is ConwayGameChain