theorem Th4: :: GOBRD12:4

for f being non constant standard special_circular_sequence holds (L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }