let A be Ordinal; :: thesis: for f, g being Sequence st A c= dom f holds
(f ^ g) | A = f | A
let f, g be Sequence; :: thesis: ( A c= dom f implies (f ^ g) | A = f | A )
assume A1: A c= dom f ; :: thesis: (f ^ g) | A = f | A
dom (f ^ g) = (dom f) +^ (dom g) by ORDINAL4:def 1;
then dom f c= dom (f ^ g) by ORDINAL3:24;
then A c= dom (f ^ g) by A1;
then A2: ( dom ((f ^ g) | A) = A & A = dom (f | A) ) by A1, RELAT_1:62;
for x being object st x in A holds
((f ^ g) | A) . x = (f | A) . x

proof

let x be object ; :: thesis: ( x in A implies ((f ^ g) | A) . x = (f | A) . x )
assume A3: x in A ; :: thesis: ((f ^ g) | A) . x = (f | A) . x
thus ((f ^ g) | A) . x = (f ^ g) . x by A3, FUNCT_1:49
.= f . x by A1, A3, ORDINAL4:def 1
.= (f | A) . x by A3, FUNCT_1:49 ; :: thesis: verum

end;

hence (f ^ g) | A = f | A by A2, FUNCT_1:2; :: thesis: verum