let D be non empty set ; :: thesis: for n, m being non zero Element of NAT
for r being Element of n -tuples_on D st m <= n & 8 <= n - m holds
Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D
let n, m be non zero Element of NAT ; :: thesis: for r being Element of n -tuples_on D st m <= n & 8 <= n - m holds
Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D
let r be Element of n -tuples_on D; :: thesis: ( m <= n & 8 <= n - m implies Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D )
assume A1: ( m <= n & 8 <= n - m ) ; :: thesis: Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D
r in { s where s is Element of D * : len s = n } ;
then consider s being Element of D * such that
A2: ( r = s & len s = n ) ;
len (Op-Right (r,m)) = n - m by A1, A2, RFINSEQ:def 1;
then len (Op-Left ((Op-Right (r,m)),8)) = 8 by A1, FINSEQ_1:59;
hence Op-Left ((Op-Right (r,m)),8) is Element of 8 -tuples_on D by FINSEQ_2:92; :: thesis: verum