let a1, a2 be Element of SCM-Data-Loc ; :: thesis: ( ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & a1 = c ) & ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & a2 = c ) implies a1 = a2 )

given c1 being Element of SCM-Data-Loc such that A2: <*c1*> = x `3_3 and

A3: a1 = c1 ; :: thesis: ( for c being Element of SCM-Data-Loc holds

( not <*c*> = x `3_3 or not a2 = c ) or a1 = a2 )

given c2 being Element of SCM-Data-Loc such that A4: ( <*c2*> = x `3_3 & a2 = c2 ) ; :: thesis: a1 = a2

thus a1 = <*c1*> /. 1 by A3, FINSEQ_4:16

.= a2 by A2, A4, FINSEQ_4:16 ; :: thesis: verum

( <*c*> = x `3_3 & a1 = c ) & ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & a2 = c ) implies a1 = a2 )

given c1 being Element of SCM-Data-Loc such that A2: <*c1*> = x `3_3 and

A3: a1 = c1 ; :: thesis: ( for c being Element of SCM-Data-Loc holds

( not <*c*> = x `3_3 or not a2 = c ) or a1 = a2 )

given c2 being Element of SCM-Data-Loc such that A4: ( <*c2*> = x `3_3 & a2 = c2 ) ; :: thesis: a1 = a2

thus a1 = <*c1*> /. 1 by A3, FINSEQ_4:16

.= a2 by A2, A4, FINSEQ_4:16 ; :: thesis: verum