let p, q be XFinSequence; :: thesis: ( p c= q implies p ^ (q /^ (len p)) = q )
assume Z: p c= q ; :: thesis: p ^ (q /^ (len p)) = q
then B: len p <= len q by NAT_1:44;
A: (len p) + (len (q /^ (len p))) = (len p) + ((len q) -' (len p)) by Def2
.= ((len q) + (len p)) -' (len p) by B, NAT_D:38
.= dom q by NAT_D:34 ;
B: for k being Nat st k in dom p holds
q . k = p . k by Z, GRFUNC_1:8;
for k being Nat st k in dom (q /^ (len p)) holds
q . ((len p) + k) = (q /^ (len p)) . k by Def2;
hence p ^ (q /^ (len p)) = q by A, B, AFINSQ_1:def 4; :: thesis: verum