let A, B be Ordinal; :: thesis: for f being Sequence holds
( f . (A +^ B) = (f /^ A) . B & ( A +^ B in dom f implies B in dom (f /^ A) ) & ( B in dom (f /^ A) implies A +^ B in dom f ) )
let f be Sequence; :: thesis: ( f . (A +^ B) = (f /^ A) . B & ( A +^ B in dom f implies B in dom (f /^ A) ) & ( B in dom (f /^ A) implies A +^ B in dom f ) )
A1: A c= A +^ B by ORDINAL3:24;
(A +^ B) -^ A = B by ORDINAL3:52;
hence ( f . (A +^ B) = (f /^ A) . B & ( A +^ B in dom f implies B in dom (f /^ A) ) & ( B in dom (f /^ A) implies A +^ B in dom f ) ) by A1, Th7; :: thesis: verum