let A be Ordinal; :: thesis: for x being Surreal
for s being Surreal-Sequence holds (s | A) + x = (s + x) | A
let x be Surreal; :: thesis: for s being Surreal-Sequence holds (s | A) + x = (s + x) | A
let s be Surreal-Sequence; :: thesis: (s | A) + x = (s + x) | A
dom (s + x) = dom s by Def17;
then A1: dom ((s + x) | A) = (dom s) /\ A by RELAT_1:61;
A2: ( (dom s) /\ A = dom (s | A) & dom (s | A) = dom ((s | A) + x) ) by Def17, RELAT_1:61;
for z being object st z in (dom s) /\ A holds
((s | A) + x) . z = ((s + x) | A) . z

proof

let z be object ; :: thesis: ( z in (dom s) /\ A implies ((s | A) + x) . z = ((s + x) | A) . z )
assume A3: z in (dom s) /\ A ; :: thesis: ((s | A) + x) . z = ((s + x) | A) . z
A4: ((s + x) | A) . z = (s + x) . z by A1, A3, FUNCT_1:47;
z in dom s by A3, XBOOLE_0:def 4;
then A5: ( s . z = s .. z & (s + x) . z = (s .. z) + x ) by Def5, Def17;
( (s | A) .. z = (s | A) . z & (s | A) . z = s . z ) by A2, A3, Def5, FUNCT_1:47;
hence ((s | A) + x) . z = ((s + x) | A) . z by A3, A4, A5, A2, Def17; :: thesis: verum

end;

hence (s | A) + x = (s + x) | A by A1, A2, FUNCT_1:2; :: thesis: verum