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, FINSEQ_1:def 8; :: thesis: verum

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, FINSEQ_1:def 8; :: thesis: verum