set f = TriangleShift2 (4,2);
set g = <*(Triangle 3)*>;
A1: len (TriangleShift2 (4,2)) = (4 - 2) - 1 by Lm26, Def15;
hence len (TriangleShift2 (4,2)) = len <*(Triangle 3)*> by CARD_1:def 7; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (TriangleShift2 (4,2)) or (TriangleShift2 (4,2)) . b₁ = <*(Triangle 3)*> . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (TriangleShift2 (4,2)) or (TriangleShift2 (4,2)) . k = <*(Triangle 3)*> . k )
assume ( 1 <= k & k <= len (TriangleShift2 (4,2)) ) ; :: thesis: (TriangleShift2 (4,2)) . k = <*(Triangle 3)*> . k
then A2: k = 1 by A1, XXREAL_0:1;
hence (TriangleShift2 (4,2)) . k = Triangle (2 + k) by A1, Def15
.= <*(Triangle 3)*> . k by A2 ;
:: thesis: verum