let A, C be Ordinal; for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A)
let xi be Ordinal-Sequence; (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 for e being object st e in dom ((C +^ xi) | A) holds
((C +^ xi) | A) . e = (C +^ (xi | A)) . elet e be
object ;
( e in dom ((C +^ xi) | A) implies ((C +^ xi) | A) . e = (C +^ (xi | A)) . e )assume A5:
e in dom ((C +^ xi) | A)
;
((C +^ xi) | A) . e = (C +^ (xi | A)) . ethen 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
;
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; verum