let a, b, c be set ; :: thesis: for D being non empty set
for f being FinSequence of D st f = <*a,b,c*> holds
( a in D & b in D & c in D )
let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b,c*> holds
( a in D & b in D & c in D )
let f be FinSequence of D; :: thesis: ( f = <*a,b,c*> implies ( a in D & b in D & c in D ) )
assume A1: f = <*a,b,c*> ; :: thesis: ( a in D & b in D & c in D )
then A2: ( len f = 3 & f . 1 = a & f . 2 = b & f . 3 = c ) by FINSEQ_1:62;
A3: ( 1 in dom f & 2 in dom f & 3 in dom f ) by A1, TOPREAL3:6;
f is Function of (dom f),D by FINSEQ_2:30;
hence ( a in D & b in D & c in D ) by A2, A3, FUNCT_2:7; :: thesis: verum