let X be non empty BCIStr_1 ; :: thesis: for d being Element of X holds the ExternalDiff of X "**" <*d*> = d
let d be Element of X; :: thesis: the ExternalDiff of X "**" <*d*> = d
A1: len <*d*> = 1 by FINSEQ_1:39;
then ex f being sequence of the carrier of X st
( f . 1 = <*d*> . 1 & ( for n being Nat st 0 <> n & n < len <*d*> holds
f . (n + 1) = the ExternalDiff of X . ((f . n),(<*d*> . (n + 1))) ) & the ExternalDiff of X "**" <*d*> = f . (len <*d*>) ) by FINSOP_1:def 1;
hence the ExternalDiff of X "**" <*d*> = d by A1; :: thesis: verum