let A, B be Ordinal; :: thesis: for f being Sequence st A c= B holds
( f . B = (f /^ A) . (B -^ A) & ( B in dom f implies B -^ A in dom (f /^ A) ) & ( B -^ A in dom (f /^ A) implies B in dom f ) )
let f be Sequence; :: thesis: ( A c= B implies ( f . B = (f /^ A) . (B -^ A) & ( B in dom f implies B -^ A in dom (f /^ A) ) & ( B -^ A in dom (f /^ A) implies B in dom f ) ) )
assume A1: A c= B ; :: thesis: ( f . B = (f /^ A) . (B -^ A) & ( B in dom f implies B -^ A in dom (f /^ A) ) & ( B -^ A in dom (f /^ A) implies B in dom f ) )
A2: f = (f | A) ^ (f /^ A) by Def1;
A3: ( B in dom f iff B -^ A in dom (f /^ A) )

proof

hereby :: thesis: ( B -^ A in dom (f /^ A) implies B in dom f )

assume B in dom f ; :: thesis: B -^ A in dom (f /^ A)
then B -^ A in (dom f) -^ A by A1, ORDINAL3:53;
hence B -^ A in dom (f /^ A) by Def1; :: thesis: verum

end;

assume B -^ A in dom (f /^ A) ; :: thesis: B in dom f
then ( B -^ A in (dom f) -^ A & not B -^ A in B -^ A ) by Def1;
then not (dom f) -^ A c= B -^ A ;
hence B in dom f by ORDINAL1:16, ORDINAL3:59; :: thesis: verum

end;

f . B = (f /^ A) . (B -^ A)

proof

per cases ( B in dom f or not B in dom f ) ;

suppose A4: B in dom f ; :: thesis: f . B = (f /^ A) . (B -^ A)

then A in dom f by A1, ORDINAL1:12;
then A c= dom f by ORDINAL1:12;
then dom (f | A) = A by RELAT_1:62;
then f . (A +^ (B -^ A)) = (f /^ A) . (B -^ A) by A2, A3, A4, ORDINAL4:def 1;
hence f . B = (f /^ A) . (B -^ A) by A1, Th3; :: thesis: verum

end;

suppose not B in dom f ; :: thesis: f . B = (f /^ A) . (B -^ A)

then ( f . B = {} & {} = (f /^ A) . (B -^ A) ) by A3, FUNCT_1:def 2;
hence f . B = (f /^ A) . (B -^ A) ; :: thesis: verum

end;

end;

end;

hence ( f . B = (f /^ A) . (B -^ A) & ( B in dom f implies B -^ A in dom (f /^ A) ) & ( B -^ A in dom (f /^ A) implies B in dom f ) ) by A3; :: thesis: verum