let a, n be Nat; ( n >= a + 1 implies TriangleShift2 ((n + 1),a) = (TriangleShift2 (n,a)) ^ <*(Triangle n)*> )
set f = TriangleShift2 ((n + 1),a);
set g = TriangleShift2 (n,a);
set h = <*H2(n)*>;
assume A1:
n >= a + 1
; TriangleShift2 ((n + 1),a) = (TriangleShift2 (n,a)) ^ <*(Triangle n)*>
then A2:
n + 1 >= a + 1
by NAT_1:13;
A3:
len (TriangleShift2 ((n + 1),a)) = ((n + 1) - a) - 1
by A2, Def15;
A4:
len (TriangleShift2 (n,a)) = (n - a) - 1
by A1, Def15;
A5:
len <*H2(n)*> = 1
by CARD_1:def 7;
A6:
len ((TriangleShift2 (n,a)) ^ <*H2(n)*>) = (len (TriangleShift2 (n,a))) + (len <*H2(n)*>)
by FINSEQ_1:22;
hence
len (TriangleShift2 ((n + 1),a)) = len ((TriangleShift2 (n,a)) ^ <*H2(n)*>)
by A3, A4, A5; FINSEQ_1:def 18 for b1 being set holds
( not 1 <= b1 or not b1 <= len (TriangleShift2 ((n + 1),a)) or (TriangleShift2 ((n + 1),a)) . b1 = ((TriangleShift2 (n,a)) ^ <*(Triangle n)*>) . b1 )
let k be Nat; ( not 1 <= k or not k <= len (TriangleShift2 ((n + 1),a)) or (TriangleShift2 ((n + 1),a)) . k = ((TriangleShift2 (n,a)) ^ <*(Triangle n)*>) . k )
assume that
A7:
1 <= k
and
A8:
k <= len (TriangleShift2 ((n + 1),a))
; (TriangleShift2 ((n + 1),a)) . k = ((TriangleShift2 (n,a)) ^ <*(Triangle n)*>) . k
A9:
(TriangleShift2 ((n + 1),a)) . k = H2(k + a)
by A2, A7, A8, Def15;
per cases
( k <= len (TriangleShift2 (n,a)) or k > len (TriangleShift2 (n,a)) )
;
suppose A11:
k > len (TriangleShift2 (n,a))
;
(TriangleShift2 ((n + 1),a)) . k = ((TriangleShift2 (n,a)) ^ <*(Triangle n)*>) . kthen
((n - a) - 1) + 1
<= k
by A4, NAT_1:13;
then
k = n - a
by A3, A8, XXREAL_0:1;
hence (TriangleShift2 ((n + 1),a)) . k =
<*H2(n)*> . (k - (len (TriangleShift2 (n,a))))
by A4, A9
.=
((TriangleShift2 (n,a)) ^ <*H2(n)*>) . k
by A3, A4, A5, A6, A8, A11, FINSEQ_1:24
;
verum end;