let a, b be set ; :: thesis: for D being non empty set
for f being FinSequence of D st f = <*a,b*> holds
f /^ 1 = <*b*>
let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b*> holds
f /^ 1 = <*b*>
let f be FinSequence of D; :: thesis: ( f = <*a,b*> implies f /^ 1 = <*b*> )
A1: f is Function of (dom f),D by FINSEQ_2:26;
assume A2: f = <*a,b*> ; :: thesis: f /^ 1 = <*b*>
then A3: ( 1 in dom f & 2 in dom f ) by CALCUL_1:14;
( f . 1 = a & f . 2 = b ) by A2;
then reconsider a2 = a, b2 = b as Element of D by A3, A1, FUNCT_2:5;
f /^ 1 = <*a2,b2*> /^ 1 by A2
.= <*b2*> by FINSEQ_6:46 ;
hence f /^ 1 = <*b*> ; :: thesis: verum