let a1, a2 be Element of SCM-Data-Loc ; ( ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a1 = b ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a2 = b ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc , b1 being Element of SCM-Data-Loc such that A5:
<*c1,f1,b1*> = x `3_3
and
A6:
a1 = b1
; ( for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc
for b being Element of SCM-Data-Loc holds
( not <*c,f,b*> = x `3_3 or not a2 = b ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc , b2 being Element of SCM-Data-Loc such that A7:
( <*c2,f2,b2*> = x `3_3 & a2 = b2 )
; a1 = a2
thus a1 =
<*c1,f1,b1*> . 3
by A6, FINSEQ_1:45
.=
a2
by A5, A7, FINSEQ_1:45
; verum