let A, C be Ordinal; :: thesis: for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A)
let xi be Ordinal-Sequence; :: thesis: (C +^ xi) | A = C +^ (xi | A)
A1: dom (xi | A) = (dom xi) /\ A by RELAT_1:61;
A2: dom (C +^ xi) = dom xi by ORDINAL3:def 1;
A3: dom ((C +^ xi) | A) = (dom (C +^ xi)) /\ A by RELAT_1:61;

A4: now :: thesis: for e being object st e in dom ((C +^ xi) | A) holds
((C +^ xi) | A) . e = (C +^ (xi | A)) . e

let e be object ; :: thesis: ( e in dom ((C +^ xi) | A) implies ((C +^ xi) | A) . e = (C +^ (xi | A)) . e )
assume A5: e in dom ((C +^ xi) | A) ; :: thesis: ((C +^ xi) | A) . e = (C +^ (xi | A)) . e
then reconsider a = e as Ordinal ;
A6: e in dom xi by A3, A2, A5, XBOOLE_0:def 4;
thus ((C +^ xi) | A) . e = (C +^ xi) . a by A5, FUNCT_1:47
.= C +^ (xi . a) by A6, ORDINAL3:def 1
.= C +^ ((xi | A) . a) by A3, A1, A2, A5, FUNCT_1:47
.= (C +^ (xi | A)) . e by A3, A1, A2, A5, ORDINAL3:def 1 ; :: thesis: verum

end;

dom (C +^ (xi | A)) = dom (xi | A) by ORDINAL3:def 1;
hence (C +^ xi) | A = C +^ (xi | A) by A1, A2, A4, FUNCT_1:2, RELAT_1:61; :: thesis: verum