let a, b be set ; :: thesis: for D being non empty set

for f being FinSequence of D st f = <*a,b*> holds

( a in D & b in D )

let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b*> holds

( a in D & b in D )

let f be FinSequence of D; :: thesis: ( f = <*a,b*> implies ( a in D & b in D ) )

A1: f is Function of (dom f),D by FINSEQ_2:26;

assume A2: f = <*a,b*> ; :: thesis: ( a in D & b in D )

then A3: ( 1 in dom f & 2 in dom f ) by CALCUL_1:14;

( f . 1 = a & f . 2 = b ) by A2, FINSEQ_1:44;

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

for f being FinSequence of D st f = <*a,b*> holds

( a in D & b in D )

let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b*> holds

( a in D & b in D )

let f be FinSequence of D; :: thesis: ( f = <*a,b*> implies ( a in D & b in D ) )

A1: f is Function of (dom f),D by FINSEQ_2:26;

assume A2: f = <*a,b*> ; :: thesis: ( a in D & b in D )

then A3: ( 1 in dom f & 2 in dom f ) by CALCUL_1:14;

( f . 1 = a & f . 2 = b ) by A2, FINSEQ_1:44;

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