let a, b be object ; :: thesis: for f being FinSequence holds
( (<*a,b*> ^ f) . 1 = a & (<*a,b*> ^ f) . 2 = b )
let f be FinSequence; :: thesis: ( (<*a,b*> ^ f) . 1 = a & (<*a,b*> ^ f) . 2 = b )
set g = <*a,b*>;
set h = <*a,b*> ^ f;
dom <*a,b*> = {1,2} by FINSEQ_1:92;
then ( 1 in dom <*a,b*> & 2 in dom <*a,b*> ) by TARSKI:def 2;
then ( (<*a,b*> ^ f) . 1 = <*a,b*> . 1 & (<*a,b*> ^ f) . 2 = <*a,b*> . 2 ) by FINSEQ_1:def 7;
hence ( (<*a,b*> ^ f) . 1 = a & (<*a,b*> ^ f) . 2 = b ) ; :: thesis: verum