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:45, 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, FINSEQ_1:45;

hence ( a in D & b in D & c in D ) by A3, A4, A1, FUNCT_2:5; :: thesis: verum

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:45, 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, FINSEQ_1:45;

hence ( a in D & b in D & c in D ) by A3, A4, A1, FUNCT_2:5; :: thesis: verum