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 ) )
A1: f is Function of (dom f),D by FINSEQ_2:26;
assume A2: f = <*a,b,c*> ; :: thesis: ( a in D & b in D & c in D )
then A3: ( f . 3 = c & 1 in dom f ) by FINSEQ_1:81;
A4: ( 2 in dom f & 3 in dom f ) by A2, FINSEQ_1:81;
( f . 1 = a & f . 2 = b ) by A2;
hence ( a in D & b in D & c in D ) by A3, A4, A1, FUNCT_2:5; :: thesis: verum