let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds
Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
let S be non empty IC-Ins-separated Mem-Struct of N; :: thesis: for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds
Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
let l1, l2, k be Nat; :: thesis: ( Start-At (l1,S) = Start-At (l2,S) implies Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S) )
assume Start-At (l1,S) = Start-At (l2,S) ; :: thesis: Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)
then {[(IC ),l1]} = Start-At (l2,S) by FUNCT_4:82
.= {[(IC ),l2]} by FUNCT_4:82 ;
then [(IC ),l1] = [(IC ),l2] by ZFMISC_1:3;
hence Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S) by ZFMISC_1:27; :: thesis: verum