let D be non empty doubleLoopStr ; :: thesis: for A being Subset of D holds A |^ 2 = A *' A
let A be Subset of D; :: thesis: A |^ 2 = A *' A
set f = <*A,(A *' A)*>;
A1: len <*A,(A *' A)*> = 2 by FINSEQ_1:44;
A2: <*A,(A *' A)*> . 1 = A ;
A3: <*A,(A *' A)*> . 2 = A *' A ;

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

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

end;

hence A |^ 2 = A *' A by A1, A2, A3, Def4; :: thesis: verum