let D be non empty doubleLoopStr ; for A being Subset of D holds A |^ 2 = A *' A
let A be Subset of D; 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
by FINSEQ_1:44;
A3:
<*A,(A *' A)*> . 2 = A *' A
by FINSEQ_1:44;
now 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;
( 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)*>
;
<*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, A3, A4, PARTFUN1:def 6;
verum end;
hence
A |^ 2 = A *' A
by A1, A2, A3, Def4; verum