let f1, f2 be FinSequence; :: thesis: for k being Nat st k in Seg ((len f1) * (len f2)) holds
( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )
let k be Nat; :: thesis: ( k in Seg ((len f1) * (len f2)) implies ( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 ) )
reconsider i1 = ((k -' 1) div (len f2)) + 1 as Nat ;
reconsider i2 = ((k -' 1) mod (len f2)) + 1 as Nat ;
assume B1: k in Seg ((len f1) * (len f2)) ; :: thesis: ( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )
then B2: ( 1 <= k & k <= (len f1) * (len f2) ) by FINSEQ_1:1;
then B3: 1 <= (len f1) * (len f2) by XXREAL_0:2;
B4: ( len f1 <> 0 & len f2 <> 0 ) by B1;
then ((k -' 1) mod (len f2)) + 1 <= len f2 by NAT_1:13, NAT_D:1;
hence ((k -' 1) mod (len f2)) + 1 in dom f2 by NAT_1:11, FINSEQ_3:25; :: thesis: ((k -' 1) div (len f2)) + 1 in dom f1
( 1 <= len f1 & 1 <= len f2 ) by B4, NAT_1:14;
then B6: (((len f1) * (len f2)) -' 1) div (len f2) = (((len f1) * (len f2)) div (len f2)) - 1 by B3, NAT_2:15, NAT_D:def 3
.= (len f1) - 1 by B4, NAT_D:18 ;
k -' 1 <= ((len f1) * (len f2)) -' 1 by B2, NAT_D:42;
then (k -' 1) div (len f2) <= (((len f1) * (len f2)) -' 1) div (len f2) by NAT_2:24;
then i1 <= ((len f1) - 1) + 1 by B6, XREAL_1:6;
hence ((k -' 1) div (len f2)) + 1 in dom f1 by NAT_1:11, FINSEQ_3:25; :: thesis: verum