let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for l1, l2 being Element of NAT
for 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 AMI-Struct of N; :: thesis: for l1, l2 being Element of NAT
for 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 be Element of NAT ; :: thesis: for k being Nat st Start-At l1,S = Start-At l2,S holds
Start-At (l1 -' k),S = Start-At (l2 -' k),S
let 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 S),l1]} = Start-At l2,S by FUNCT_4:87;
then {[(IC S),l1]} = {[(IC S),l2]} by FUNCT_4:87;
then [(IC S),l1] = [(IC S),l2] by ZFMISC_1:6;
hence Start-At (l1 -' k),S = Start-At (l2 -' k),S by ZFMISC_1:33; :: thesis: verum