let p, q be FinSequence; :: thesis: ( p c= q implies q | (len p) = p )
assume A1: p c= q ; :: thesis: q | (len p) = p
A2: for k being Nat st k in dom p holds
p . k = (q | (len p)) . k
proof
let k be Nat; :: thesis: ( k in dom p implies p . k = (q | (len p)) . k )
assume A3: k in dom p ; :: thesis: p . k = (q | (len p)) . k
then A4: k <= len p by Th25;
thus p . k = q . k by A1, A3, GRFUNC_1:2
.= (q | (len p)) . k by A4, Th110 ; :: thesis: verum
end;
len p <= len q by A1, FINSEQ_1:63;
then len (q | (len p)) = len p by FINSEQ_1:59;
then dom (q | (len p)) = dom p by Th27;
hence q | (len p) = p by A2; :: thesis: verum