let D be non empty set ; for p1, p2, p3 being Element of D st p2 <> p3 holds
Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>
let p1, p2, p3 be Element of D; ( p2 <> p3 implies Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> )
assume A1:
p2 <> p3
; Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>
per cases
( p1 = p3 or p1 <> p3 )
;
suppose A2:
p1 <> p3
;
Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>
rng <*p1,p2,p3*> = {p1,p2,p3}
by Lm2;
then
p3 in rng <*p1,p2,p3*>
by ENUMSET1:def 1;
hence Rotate (
<*p1,p2,p3*>,
p3) =
(<*p1,p2,p3*> :- p3) ^ ((<*p1,p2,p3*> -: p3) /^ 1)
by Def2
.=
<*p3*> ^ ((<*p1,p2,p3*> -: p3) /^ 1)
by A1, A2, Th55
.=
<*p3*> ^ (<*p1,p2,p3*> /^ 1)
by A1, A2, Th51
.=
<*p3*> ^ <*p2,p3*>
by Th47
.=
<*p3,p2,p3*>
by FINSEQ_1:43
;
verum end; end;