let X be set ; :: thesis: for fs, fs1, fs2 being FinSequence of X
for fss, fss2 being Subset of fs
for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds
Seq fss2 = fs2

let fs, fs1, fs2 be FinSequence of X; :: thesis: for fss, fss2 being Subset of fs
for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds
Seq fss2 = fs2

let fss, fss2 be Subset of fs; :: thesis: for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds
Seq fss2 = fs2

let fss1 be Subset of fs1; :: thesis: ( Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) implies Seq fss2 = fs2 )
assume that
A1: Seq fss = fs1 and
A2: Seq fss1 = fs2 and
A3: fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) ; :: thesis: Seq fss2 = fs2
consider k being Nat such that
A4: dom fs = Seg k by FINSEQ_1:def 2;
reconsider d2 = dom fss2 as finite set ;
reconsider d1 = dom fss1 as finite set ;
A5: ex l being Nat st dom fs1 = Seg l by FINSEQ_1:def 2;
then A6: dom (Sgm d1) = Seg (card d1) by ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A7: dom fss c= Seg k by ;
then rng (Sgm (dom fss)) c= dom fss by FINSEQ_1:def 13;
then A8: dom fs1 = dom (Sgm (dom fss)) by ;
dom fss2 c= Seg k by ;
then A9: rng (Sgm (dom fss2)) = dom fss2 by FINSEQ_1:def 13;
A10: (Sgm (dom fss)) | (dom fss1) c= Sgm (dom fss) by RELAT_1:59;
then A11: dom ((Sgm (dom fss)) | (dom fss1)) c= dom (Sgm (dom fss)) by RELAT_1:11;
rng ((Sgm (dom fss)) | (dom fss1)) c= rng (Sgm (dom fss)) by ;
then rng ((Sgm (dom fss)) | (dom fss1)) c= dom fss by ;
then A12: dom fss2 = rng ((Sgm (dom fss)) | (dom fss1)) by ;
A13: dom fss1 c= dom fs1 by RELAT_1:11;
now :: thesis: ex Z being Element of bool st
( ( for x being object st x in d1 holds
ex y being object st
( y in d2 & [x,y] in Z ) ) & ( for y being object st y in d2 holds
ex x being object st
( x in d1 & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( ( x = z implies y = u ) & ( y = u implies not x <> z ) ) ) )
take Z = (Sgm (dom fss)) | (dom fss1); :: thesis: ( ( for x being object st x in d1 holds
ex y being object st
( y in d2 & [x,y] in Z ) ) & ( for y being object st y in d2 holds
ex x being object st
( x in d1 & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( ( x = z implies y = u ) & ( y = u implies not x <> z ) ) ) )

A14: dom Z = dom fss1 by ;
hereby :: thesis: ( ( for y being object st y in d2 holds
ex x being object st
( x in d1 & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( ( x = z implies y = u ) & ( y = u implies not x <> z ) ) ) )
let x be object ; :: thesis: ( x in d1 implies ex y being object st
( y in d2 & [x,y] in Z ) )

assume A15: x in d1 ; :: thesis: ex y being object st
( y in d2 & [x,y] in Z )

reconsider y = Z . x as object ;
take y = y; :: thesis: ( y in d2 & [x,y] in Z )
thus y in d2 by ; :: thesis: [x,y] in Z
thus [x,y] in Z by ; :: thesis: verum
end;
hereby :: thesis: for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( ( x = z implies y = u ) & ( y = u implies not x <> z ) )
let y be object ; :: thesis: ( y in d2 implies ex x being object st
( x in d1 & [x,y] in Z ) )

assume y in d2 ; :: thesis: ex x being object st
( x in d1 & [x,y] in Z )

then consider x being object such that
A16: x in dom Z and
A17: y = Z . x by ;
reconsider x = x as object ;
take x = x; :: thesis: ( x in d1 & [x,y] in Z )
thus ( x in d1 & [x,y] in Z ) by ; :: thesis: verum
end;
let x, y, z, u be object ; :: thesis: ( [x,y] in Z & [z,u] in Z implies ( ( x = z implies y = u ) & ( y = u implies not x <> z ) ) )
assume that
A18: [x,y] in Z and
A19: [z,u] in Z ; :: thesis: ( ( x = z implies y = u ) & ( y = u implies not x <> z ) )
A20: z in dom Z by ;
A21: u = Z . z by ;
A22: u = (Sgm (dom fss)) . z by ;
A23: y = Z . x by ;
hence ( x = z implies y = u ) by ; :: thesis: ( y = u implies not x <> z )
A24: x in dom Z by ;
then A25: y = (Sgm (dom fss)) . x by ;
assume A26: y = u ; :: thesis: not x <> z
assume A27: x <> z ; :: thesis: contradiction
reconsider x = x, z = z as Element of NAT by ;
A28: x <= len (Sgm (dom fss)) by ;
A29: z <= len (Sgm (dom fss)) by ;
A30: 1 <= z by ;
A31: 1 <= x by ;
per cases ( x < z or z < x ) by ;
end;
end;
then d1,d2 are_equipotent ;
then card d1 = card d2 by CARD_1:5;
then A32: dom (Sgm d2) = Seg (card d1) by ;
A33: rng (Sgm (dom fss1)) = dom fss1 by ;
now :: thesis: ( dom fs2 = dom (Seq fss2) & dom fs2 = dom fs2 & ( for k being Nat st k in dom fs2 holds
(Seq fss2) . k = fs2 . k ) )
now :: thesis: for x being object holds
( ( x in dom fs2 implies x in dom (Seq fss2) ) & ( x in dom (Seq fss2) implies x in dom fs2 ) )
let x be object ; :: thesis: ( ( x in dom fs2 implies x in dom (Seq fss2) ) & ( x in dom (Seq fss2) implies x in dom fs2 ) )
hereby :: thesis: ( x in dom (Seq fss2) implies x in dom fs2 )
assume x in dom fs2 ; :: thesis: x in dom (Seq fss2)
then A34: x in dom (Sgm (dom fss2)) by ;
then (Sgm (dom fss2)) . x in dom fss2 by ;
hence x in dom (Seq fss2) by ; :: thesis: verum
end;
assume x in dom (Seq fss2) ; :: thesis: x in dom fs2
then A35: x in dom (Sgm (dom fss1)) by ;
then (Sgm (dom fss1)) . x in dom fss1 by ;
hence x in dom fs2 by ; :: thesis: verum
end;
hence A36: dom fs2 = dom (Seq fss2) by TARSKI:2; :: thesis: ( dom fs2 = dom fs2 & ( for k being Nat st k in dom fs2 holds
(Seq fss2) . k = fs2 . k ) )

thus dom fs2 = dom fs2 ; :: thesis: for k being Nat st k in dom fs2 holds
(Seq fss2) . k = fs2 . k

let k be Nat; :: thesis: ( k in dom fs2 implies (Seq fss2) . k = fs2 . k )
assume A37: k in dom fs2 ; :: thesis: (Seq fss2) . k = fs2 . k
then A38: (Sgm (dom fss1)) . k in dom fss1 by ;
A39: (Sgm (dom fss2)) . k in dom fss2 by ;
A40: (Sgm (dom fss1)) . k in dom fss1 by ;
then A41: fss1 . ((Sgm (dom fss1)) . k) = (Seq fss) . ((Sgm (dom fss1)) . k) by ;
A42: (Sgm (dom fss2)) . k = ((Sgm (dom fss)) * (Sgm (dom fss1))) . k by ;
k in dom (Sgm (dom fss1)) by ;
then k in dom ((Sgm (dom fss)) * (Sgm (dom fss1))) by ;
then A43: (Sgm (dom fss2)) . k = (Sgm (dom fss)) . ((Sgm (dom fss1)) . k) by ;
A44: fss2 c= fss by ;
dom fss1 c= dom (Seq fss) by ;
then A45: (Sgm (dom fss1)) . k in dom (Sgm (dom fss)) by ;
thus (Seq fss2) . k = fss2 . ((Sgm (dom fss2)) . k) by
.= fss . ((Sgm (dom fss)) . ((Sgm (dom fss1)) . k)) by
.= fss1 . ((Sgm (dom fss1)) . k) by
.= fs2 . k by ; :: thesis: verum
end;
hence Seq fss2 = fs2 by FINSEQ_1:13; :: thesis: verum