let D be non empty set ; :: thesis: for w being non empty FinSequence of D holds (D -firstChar) . w = w . 1
let w be non empty FinSequence of D; :: thesis: (D -firstChar) . w = w . 1
consider d being Element of D, df1 being FinSequence of D such that
A1: ( d = w . 1 & w = <*d*> ^ df1 ) by FINSEQ_3:102;
set f = D -pr1 ;
set F = MultPlace (D -pr1);

per cases ( len w <= 1 or len w > 1 ) ;

suppose len w <= 1 ; :: thesis: (D -firstChar) . w = w . 1

then ( len w <= 0 or len w = 0 + 1 ) by NAT_1:8;
then w = <*d*> by A1, FINSEQ_1:40;
hence (D -firstChar) . w = w . 1 by Lm15; :: thesis: verum

end;

suppose A2: len w > 1 ; :: thesis: (D -firstChar) . w = w . 1

len w = (len <*d*>) + (len df1) by A1, FINSEQ_1:22
.= 1 + (len df1) by FINSEQ_1:40 ;
then len df1 <> 0 by A2;
then consider k being Nat such that
A3: len df1 = k + 1 by NAT_1:6;
reconsider df11 = df1 as Element of (k + 1) -tuples_on D by A3, FINSEQ_2:133;
reconsider df111 = df11 as Element of (D *) \ {{}} by Th5;
(MultPlace (D -pr1)) . w = (pr1 (D,D)) . (d,((MultPlace (D -pr1)) . df111)) by A1, Lm17
.= w . 1 by FUNCT_3:def 4, A1 ;
hence (D -firstChar) . w = w . 1 ; :: thesis: verum

end;

end;