let a, b, c be set ; 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 ; 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; ( 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*>
; ( 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; verum