let x be set ; :: 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:87, TARSKI:def 1;
then 0 in dom <%x%> by Def5;
then (<%x%> ^ p) . 0 = <%x%> . 0 by Def4;
hence (<%x%> ^ p) . 0 = x by Def5; :: thesis: verum