let x be object ; :: thesis: for p being XFinSequence holds (<%x%> ^ p) . 0 = x
let p be XFinSequence; :: thesis: (<%x%> ^ p) . 0 = x
0 in 1 by CARD_1:49, TARSKI:def 1;
then 0 in dom <%x%> by Def4;
then (<%x%> ^ p) . 0 = <%x%> . 0 by Def3;
hence (<%x%> ^ p) . 0 = x ; :: thesis: verum