let p be XFinSequence; :: thesis: for e being object holds dom (Shift (<%e%>,(card p))) = {(card p)}
let e be object ; :: thesis: dom (Shift (<%e%>,(card p))) = {(card p)}
for u being object holds
( u in dom (Shift (<%e%>,(card p))) iff u = card p )

proof

let u be object ; :: thesis: ( u in dom (Shift (<%e%>,(card p))) iff u = card p )
thus ( u in dom (Shift (<%e%>,(card p))) implies u = card p ) :: thesis: ( u = card p implies u in dom (Shift (<%e%>,(card p))) )

proof

assume u in dom (Shift (<%e%>,(card p))) ; :: thesis: u = card p
then u in { (m + (card p)) where m is Nat : m in dom <%e%> } by VALUED_1:def 12;
then consider m being Nat such that
A1: u = m + (card p) and
A2: m in dom <%e%> ;
m = 0 by A2, TARSKI:def 1;
hence u = card p by A1; :: thesis: verum

end;

0 in 1 by CARD_1:49, TARSKI:def 1;
then 0 in dom <%e%> by Def4;
then 0 + (card p) in dom (Shift (<%e%>,(card p))) by VALUED_1:24;
hence ( u = card p implies u in dom (Shift (<%e%>,(card p))) ) ; :: thesis: verum

end;

hence dom (Shift (<%e%>,(card p))) = {(card p)} by TARSKI:def 1; :: thesis: verum