let a1, a2 be Element of SCM+FSA-Data*-Loc ; :: thesis: ( 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 = f ) & 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 = f ) 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 A8: <*c1,f1,b1*> = x `3_3 and

A9: a1 = f1 ; :: thesis: ( 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 = f ) 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 A10: ( <*c2,f2,b2*> = x `3_3 & a2 = f2 ) ; :: thesis: a1 = a2

thus a1 = <*c1,f1,b1*> . 2 by A9, FINSEQ_1:45

.= a2 by A8, A10, FINSEQ_1:45 ; :: thesis: verum

( <*c,f,b*> = x `3_3 & a1 = f ) & 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 = f ) 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 A8: <*c1,f1,b1*> = x `3_3 and

A9: a1 = f1 ; :: thesis: ( 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 = f ) 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 A10: ( <*c2,f2,b2*> = x `3_3 & a2 = f2 ) ; :: thesis: a1 = a2

thus a1 = <*c1,f1,b1*> . 2 by A9, FINSEQ_1:45

.= a2 by A8, A10, FINSEQ_1:45 ; :: thesis: verum