let A be Ordinal; :: thesis: for f, g being Sequence st dom f c= A holds
(f ^ g) | A = f ^ (g | (A -^ (dom f)))
let f, g be Sequence; :: thesis: ( dom f c= A implies (f ^ g) | A = f ^ (g | (A -^ (dom f))) )
assume A1: dom f c= A ; :: thesis: (f ^ g) | A = f ^ (g | (A -^ (dom f)))

per cases ( A c= dom (f ^ g) or dom (f ^ g) c= A ) ;

suppose A2: A c= dom (f ^ g) ; :: thesis: (f ^ g) | A = f ^ (g | (A -^ (dom f)))

then A3: dom ((f ^ g) | A) = A by RELAT_1:62;
set B = A -^ (dom f);
A4: dom (f ^ g) = (dom f) +^ (dom g) by ORDINAL4:def 1;
( A -^ (dom f) c= (dom (f ^ g)) -^ (dom f) & (dom (f ^ g)) -^ (dom f) = dom g ) by A4, A2, ORDINAL3:52, ORDINAL3:59;
then A5: dom (g | (A -^ (dom f))) = A -^ (dom f) by RELAT_1:62;
then A6: ( dom (f ^ (g | (A -^ (dom f)))) = (dom f) +^ (A -^ (dom f)) & (dom f) +^ (A -^ (dom f)) = A ) by A1, ORDINAL4:def 1, Th3;
for x being object st x in A holds
((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x

proof

let x be object ; :: thesis: ( x in A implies ((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x )
assume A7: x in A ; :: thesis: ((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x
reconsider X = x as Ordinal by A7;
A8: ((f ^ g) | A) . x = (f ^ g) . x by A7, FUNCT_1:49;

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

suppose x in dom f ; :: thesis: ((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x

then ( (f ^ g) . x = f . x & f . x = (f ^ (g | (A -^ (dom f)))) . x ) by ORDINAL4:def 1;
hence ((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x by A7, FUNCT_1:49; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: ((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x

then A9: dom f c= X by ORDINAL1:16;
then ( X -^ (dom f) in A -^ (dom f) & (dom f) +^ (X -^ (dom f)) = x ) by A7, ORDINAL3:53, Th3;
then A10: ( (f ^ (g | (A -^ (dom f)))) . x = (g | (A -^ (dom f))) . (X -^ (dom f)) & (g | (A -^ (dom f))) . (X -^ (dom f)) = g . (X -^ (dom f)) ) by FUNCT_1:49, A5, ORDINAL4:def 1;
( X -^ (dom f) in (dom (f ^ g)) -^ (dom f) & (dom (f ^ g)) -^ (dom f) = dom g & (dom f) +^ (X -^ (dom f)) = X ) by A9, A4, A2, A7, Th3, ORDINAL3:52, ORDINAL3:53;
hence ((f ^ g) | A) . x = (f ^ (g | (A -^ (dom f)))) . x by A8, A10, ORDINAL4:def 1; :: thesis: verum

end;

end;

end;

hence (f ^ g) | A = f ^ (g | (A -^ (dom f))) by A3, A6, FUNCT_1:2; :: thesis: verum

end;

suppose A11: dom (f ^ g) c= A ; :: thesis: (f ^ g) | A = f ^ (g | (A -^ (dom f)))

then A12: (f ^ g) | A = f ^ g by RELAT_1:68;
dom (f ^ g) = (dom f) +^ (dom g) by ORDINAL4:def 1;
then ( dom g = ((dom f) +^ (dom g)) -^ (dom f) & ((dom f) +^ (dom g)) -^ (dom f) c= A -^ (dom f) ) by A11, ORDINAL3:52, ORDINAL3:59;
hence (f ^ g) | A = f ^ (g | (A -^ (dom f))) by A12, RELAT_1:68; :: thesis: verum

end;

end;