let a1, a2 be Element of SCM+FSA-Data-Loc ; :: thesis: ( ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & a1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & a2 = c ) implies a1 = a2 )
given c1 being Element of SCM+FSA-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc such that A2: <*c1,f1*> = x `2 and
A3: a1 = c1 ; :: thesis: ( for c being Element of SCM+FSA-Data-Loc
for f being Element of SCM+FSA-Data*-Loc holds
( not <*c,f*> = x `2 or not a2 = c ) or a1 = a2 )
given c2 being Element of SCM+FSA-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc such that A4: <*c2,f2*> = x `2 and
A5: a2 = c2 ; :: thesis: a1 = a2
thus a1 = <*c1,f1*> /. 1 by A3, FINSEQ_4:26
.= a2 by A2, A4, A5, FINSEQ_4:26 ; :: thesis: verum