let y be Surreal-Sequence; :: thesis: for A being Ordinal holds No_omega^ (y | A) = (No_omega^ y) | A
let A be Ordinal; :: thesis: No_omega^ (y | A) = (No_omega^ y) | A
A1: dom (No_omega^ y) = dom y by Def22;
then A2: dom ((No_omega^ y) | A) = (dom y) /\ A by RELAT_1:61;
A3: ( dom (No_omega^ (y | A)) = dom (y | A) & dom (y | A) = (dom y) /\ A ) by Def22, RELAT_1:61;
for x being object st x in (dom y) /\ A holds
(No_omega^ (y | A)) . x = ((No_omega^ y) | A) . x

proof

let x be object ; :: thesis: ( x in (dom y) /\ A implies (No_omega^ (y | A)) . x = ((No_omega^ y) | A) . x )
assume A4: x in (dom y) /\ A ; :: thesis: (No_omega^ (y | A)) . x = ((No_omega^ y) | A) . x
then A5: ( x in dom y & x in A ) by XBOOLE_0:def 4;
then y . x in rng y by FUNCT_1:def 3;
then reconsider yx = y . x as Surreal by SURREAL0:def 16;
(y | A) . x = y . x by A5, FUNCT_1:49;
hence (No_omega^ (y | A)) . x = No_omega^ yx by A3, A4, Def22
.= (No_omega^ y) . x by A1, A5, Def22
.= ((No_omega^ y) | A) . x by A5, FUNCT_1:49 ;
:: thesis: verum

end;

hence No_omega^ (y | A) = (No_omega^ y) | A by A2, A3, FUNCT_1:2; :: thesis: verum