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