let X be non empty set ; :: thesis: for s being sequence of X holds s ^\ 0 = s
let s be sequence of X; :: thesis: s ^\ 0 = s

now :: thesis: for n being Element of NAT holds (s ^\ 0) . n = s . n

let n be Element of NAT ; :: thesis: (s ^\ 0) . n = s . n
thus (s ^\ 0) . n = s . (n + 0) by Def2
.= s . n ; :: thesis: verum

end;

hence s ^\ 0 = s by FUNCT_2:63; :: thesis: verum