let f1, f2 be ConwayGameChain; :: thesis: ( ex g being ConwayGame st
( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) implies f1 ^ f2 is ConwayGameChain )
assume A1: ex g being ConwayGame st
( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) ; :: thesis: f1 ^ f2 is ConwayGameChain
then reconsider g = f2 . 1 as ConwayGame ;
f1 ^ f2 is ConwayGame-valued
proof
let x be set ; :: according to CGAMES_1:def 10 :: thesis: ( x in dom (f1 ^ f2) implies (f1 ^ f2) . x is ConwayGame )
set y = (f1 ^ f2) . x;
assume x in dom (f1 ^ f2) ; :: thesis: (f1 ^ f2) . x is ConwayGame
then (f1 ^ f2) . x in rng (f1 ^ f2) by FUNCT_1:3;
then A2: (f1 ^ f2) . x in (rng f1) \/ (rng f2) by FINSEQ_1:31;
per cases ( (f1 ^ f2) . x in rng f1 or (f1 ^ f2) . x in rng f2 ) by A2, XBOOLE_0:def 3;
suppose (f1 ^ f2) . x in rng f1 ; :: thesis: (f1 ^ f2) . x is ConwayGame
then ex z being object st
( z in dom f1 & (f1 ^ f2) . x = f1 . z ) by FUNCT_1:def 3;
hence (f1 ^ f2) . x is ConwayGame ; :: thesis: verum
end;
suppose (f1 ^ f2) . x in rng f2 ; :: thesis: (f1 ^ f2) . x is ConwayGame
then ex z being object st
( z in dom f2 & (f1 ^ f2) . x = f2 . z ) by FUNCT_1:def 3;
hence (f1 ^ f2) . x is ConwayGame ; :: thesis: verum
end;
end;
end;
then reconsider f12 = f1 ^ f2 as non empty ConwayGame-valued FinSequence ;
f12 is ConwayGameChain-like
proof
let n be Element of dom f12; :: according to CGAMES_1:def 11 :: thesis: ( n > 1 implies f12 . (n - 1) in the_Options_of (f12 . n) )
assume A3: n > 1 ; :: thesis: f12 . (n - 1) in the_Options_of (f12 . n)
per cases ( n < (len f1) + 1 or n = (len f1) + 1 or n > (len f1) + 1 ) by XXREAL_0:1;
suppose n < (len f1) + 1 ; :: thesis: f12 . (n - 1) in the_Options_of (f12 . n)
then n <= len f1 by NAT_1:22;
then reconsider n0 = n as Element of dom f1 by A3, FINSEQ_3:25;
n0 - 1 in dom f1 by Th20, A3;
then ( f1 . n0 = f12 . n0 & f1 . (n0 - 1) = f12 . (n0 - 1) ) by FINSEQ_1:def 7;
hence f12 . (n - 1) in the_Options_of (f12 . n) by A3, Def11; :: thesis: verum
end;
suppose A4: n = (len f1) + 1 ; :: thesis: f12 . (n - 1) in the_Options_of (f12 . n)
( len f1 in dom f1 & 1 in dom f2 ) by FINSEQ_5:6;
then ( f12 . (n - 1) = f1 . (len f1) & f12 . n = f2 . 1 ) by A4, FINSEQ_1:def 7;
hence f12 . (n - 1) in the_Options_of (f12 . n) by A1; :: thesis: verum
end;
suppose A5: n > (len f1) + 1 ; :: thesis: f12 . (n - 1) in the_Options_of (f12 . n)
( n <= len f12 & len f12 = (len f1) + (len f2) & n >= len f1 ) by A5, FINSEQ_1:22, FINSEQ_3:25, XREAL_1:38;
then A6: ( n - (len f1) > 1 & n - (len f1) <= len f2 & n - (len f1) is Nat ) by A5, NAT_1:21, XREAL_1:20;
then reconsider k = n - (len f1) as Element of dom f2 by FINSEQ_3:25;
k - 1 in dom f2 by A6, Th20;
then ( f12 . ((len f1) + k) = f2 . k & f12 . ((len f1) + (k - 1)) = f2 . (k - 1) ) by FINSEQ_1:def 7;
hence f12 . (n - 1) in the_Options_of (f12 . n) by A6, Def11; :: thesis: verum
end;
end;
end;
hence f1 ^ f2 is ConwayGameChain ; :: thesis: verum