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*> )
assume A1: f = <*a,b*> ; :: thesis: f /^ 1 = <*b*>
then A2: ( len f = 2 & f . 1 = a & f . 2 = b ) by FINSEQ_1:61;
A3: ( 1 in dom f & 2 in dom f ) by A1, CALCUL_1:14;
f is Function of (dom f),D by FINSEQ_2:30;
then reconsider a2 = a, b2 = b as Element of D by A2, A3, FUNCT_2:7;
f /^ 1 = <*a2,b2*> /^ 1 by A1
.= <*b2*> by FINSEQ_6:50 ;
hence f /^ 1 = <*b*> ; :: thesis: verum