let f be Sequence; :: thesis: for g1, g2 being Sequence st f ^ g1 = f ^ g2 holds
g1 = g2
let g1, g2 be Sequence; :: thesis: ( f ^ g1 = f ^ g2 implies g1 = g2 )
assume A1: f ^ g1 = f ^ g2 ; :: thesis: g1 = g2
( dom (f ^ g2) = (dom f) +^ (dom g2) & dom (f ^ g1) = (dom f) +^ (dom g1) ) by ORDINAL4:def 1;
then A2: dom g1 = ((dom f) +^ (dom g2)) -^ (dom f) by A1, ORDINAL3:52
.= dom g2 by ORDINAL3:52 ;
for x being object st x in dom g1 holds
g1 . x = g2 . x

proof

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A3: x in dom g1 ; :: thesis: g1 . x = g2 . x
reconsider X = x as Ordinal by A3;
thus g1 . x = (f ^ g1) . ((dom f) +^ X) by A3, ORDINAL4:def 1
.= g2 . x by A1, A2, A3, ORDINAL4:def 1 ; :: thesis: verum

end;

hence g1 = g2 by A2, FUNCT_1:2; :: thesis: verum