let p, q be FinSequence; :: thesis: ( not p is empty implies (p ^ q) . 1 = p . 1 )
assume not p is empty ; :: thesis: (p ^ q) . 1 = p . 1
then reconsider p = p as non empty FinSequence ;
set n = len p;
( 1 <= 1 & 1 <= len p ) by NAT_1:14;
then 1 in Seg (len p) ;
then 1 in dom p by FINSEQ_1:def 3;
hence (p ^ q) . 1 = p . 1 by FINSEQ_1:def 7; :: thesis: verum