let D be non empty set ; :: thesis: for a being Element of D holds <*<*a*>*> is Matrix of 1,D
let a be Element of D; :: thesis: <*<*a*>*> is Matrix of 1,D
len <*a*> = 1 by FINSEQ_1:39;
hence <*<*a*>*> is Matrix of 1,D by Th11; :: thesis: verum