let D be non empty doubleLoopStr ; :: thesis: for A being Subset of D holds A |^ 1 = A
let A be Subset of D; :: thesis: A |^ 1 = A
set f = <*A*>;
A1: ( len <*A*> = 1 & <*A*> . 1 = A ) by FINSEQ_1:40;

now :: thesis: for i being Nat st i in dom <*A*> & i + 1 in dom <*A*> holds
<*A*> . (i + 1) = A *' (<*A*> /. i)

let i be Nat; :: thesis: ( i in dom <*A*> & i + 1 in dom <*A*> implies <*A*> . (i + 1) = A *' (<*A*> /. i) )
assume A2: ( i in dom <*A*> & i + 1 in dom <*A*> ) ; :: thesis: <*A*> . (i + 1) = A *' (<*A*> /. i)
dom <*A*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then ( i = 1 & i + 1 = 1 ) by A2, TARSKI:def 1;
hence <*A*> . (i + 1) = A *' (<*A*> /. i) ; :: thesis: verum

end;

hence A |^ 1 = A by A1, Def4; :: thesis: verum