let D be non empty set ; :: thesis: for d1, d2, d3 being Element of D holds <*d1,d2,d3*> is FinSequence of D
let d1, d2, d3 be Element of D; :: thesis: <*d1,d2,d3*> is FinSequence of D
( rng <*d1,d2,d3*> = {d1,d2,d3} & {d1,d2,d3} c= D ) by Lm3;
hence <*d1,d2,d3*> is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum