let n be non empty Nat; :: thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let F be Group-like associative multMagma-Family of Seg n; :: thesis: for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let x be Element of (product F); :: thesis: for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let s, t be FinSequence of (product F); :: thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t implies s = t )
set I = Seg n;
assume that
A1: len s = n and
A2: for k being Element of Seg n holds s . k in ProjGroup (F,k) and
A3: x = Product s and
B1: len t = n and
B2: for k being Element of Seg n holds t . k in ProjGroup (F,k) and
B3: x = Product t ; :: thesis: s = t

now

let i be Nat; :: thesis: ( 1 <= i & i <= n implies s . i = t . i )
assume P1: ( 1 <= i & i <= n ) ; :: thesis: s . i = t . i
then reconsider i0 = i as Element of Seg n by FINSEQ_1:3;
consider si being Element of (product F) such that
P2: ( si = s . i & x . i = si . i ) by A1, A2, A3, P1, LMP500;
consider ti being Element of (product F) such that
P3: ( ti = t . i & x . i = ti . i ) by B1, B2, B3, P1, LMP500;
s . i0 in ProjGroup (F,i0) by A2;
then s . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def 5;
then P4: s . i0 in ProjSet (F,i0) by defPrjGroup;
consider sn being Function, gn being Element of (F . i0) such that
P5: ( sn = si & dom sn = Seg n & sn . i0 = gn & ( for k being Element of Seg n st k <> i0 holds
sn . k = 1_ (F . k) ) ) by P2, P4, LMP1;
t . i0 in ProjGroup (F,i0) by B2;
then t . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def 5;
then Q4: t . i0 in ProjSet (F,i0) by defPrjGroup;
consider tn being Function, fn being Element of (F . i0) such that
Q5: ( tn = ti & dom tn = Seg n & tn . i0 = fn & ( for k being Element of Seg n st k <> i0 holds
tn . k = 1_ (F . k) ) ) by P3, Q4, LMP1;

now

let x be set ; :: thesis: ( x in dom sn implies sn . b₁ = tn . b₁ )
assume x in dom sn ; :: thesis: sn . b₁ = tn . b₁
then reconsider j = x as Element of Seg n by P5;

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: sn . b₁ = tn . b₁

hence sn . x = tn . x by P2, P3, P5, Q5; :: thesis: verum

end;

suppose XX3: j <> i ; :: thesis: sn . b₁ = tn . b₁

then sn . j = 1_ (F . j) by P5;
hence sn . x = tn . x by XX3, Q5; :: thesis: verum

end;

end;

end;

hence s . i = t . i by P2, P3, P5, Q5, FUNCT_1:9; :: thesis: verum

end;

hence s = t by A1, B1, FINSEQ_1:18; :: thesis: verum