let D be non empty set ; :: thesis: for m, n, l being non zero Element of NAT
for s being Element of n -tuples_on D st m <= n & l = n - m holds
Op-Right (s,m) is Element of l -tuples_on D
let m, n, l be non zero Element of NAT ; :: thesis: for s being Element of n -tuples_on D st m <= n & l = n - m holds
Op-Right (s,m) is Element of l -tuples_on D
let s be Element of n -tuples_on D; :: thesis: ( m <= n & l = n - m implies Op-Right (s,m) is Element of l -tuples_on D )
assume A1: ( m <= n & l = n - m ) ; :: thesis: Op-Right (s,m) is Element of l -tuples_on D
len s = n by CARD_1:def 7;
then len (Op-Right (s,m)) = l by A1, RFINSEQ:def 1;
then Op-Right (s,m) is Tuple of l,D by CARD_1:def 7;
hence Op-Right (s,m) is Element of l -tuples_on D by FINSEQ_2:131; :: thesis: verum