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