theorem :: BCIALG_4:29

for X being non empty BCIStr_1
for d being Element of X holds the ExternalDiff of X "**" <*d*> = d