let f be ConwayGameChain; :: thesis: for n being non zero Nat holds f | n is ConwayGameChain
let n be non zero Nat; :: thesis: f | n is ConwayGameChain
set ls = len (f | n);
A1: f | n is ConwayGame-valued
proof
let x be set ; :: according to CGAMES_1:def 10 :: thesis: ( x in dom (f | n) implies (f | n) . x is ConwayGame )
assume A2: x in dom (f | n) ; :: thesis: (f | n) . x is ConwayGame
dom (f | n) c= dom f by RELAT_1:60;
then f . x is ConwayGame by A2;
hence (f | n) . x is ConwayGame by A2, FUNCT_1:47; :: thesis: verum
end;
reconsider fs = f | n as non empty ConwayGame-valued FinSequence by A1;
fs is ConwayGameChain-like
proof
let n be Element of dom fs; :: according to CGAMES_1:def 11 :: thesis: ( n > 1 implies fs . (n - 1) in the_Options_of (fs . n) )
assume A3: n > 1 ; :: thesis: fs . (n - 1) in the_Options_of (fs . n)
( dom fs c= dom f & n in dom fs & n - 1 in dom fs ) by Th20, A3, RELAT_1:60;
then ( n in dom f & f . n = fs . n & f . (n - 1) = fs . (n - 1) ) by FUNCT_1:47;
hence fs . (n - 1) in the_Options_of (fs . n) by Def11, A3; :: thesis: verum
end;
hence f | n is ConwayGameChain ; :: thesis: verum