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

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

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

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