let p, q be XFinSequence; :: thesis: ( p c= q implies p ^ (q /^ (len p)) = q )
assume A1: p c= q ; :: thesis: p ^ (q /^ (len p)) = q
A2: (len p) + (len (q /^ (len p))) = (len p) + ((len q) -' (len p)) by Def2
.= ((len q) + (len p)) -' (len p) by A1, NAT_1:43, NAT_D:38
.= dom q by NAT_D:34 ;
A3: for k being Nat st k in dom p holds
q . k = p . k by A1, GRFUNC_1:2;
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 A2, A3, AFINSQ_1:def 3; :: thesis: verum