let X be set ; :: thesis:
let fs, fs1, fs2 be FinSequence of X; :: thesis:
let fss, fss2 be Subset of fs; :: thesis:
let fss1 be Subset of fs1; :: thesis:
assume that
A1: Seq fss = fs1 and
A2: Seq fss1 = fs2 and
A3: fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) ; :: thesis:
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 FINSEQ_3:40, RELAT_1:11;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A7: dom fss c= Seg k by A4, RELAT_1:11;
then rng (Sgm (dom fss)) c= dom fss by FINSEQ_1:def 13;
then A8: dom fs1 = dom (Sgm (dom fss)) by A1, RELAT_1:27;
dom fss2 c= Seg k by A4, RELAT_1:11;
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 A10, RELAT_1:11;
then rng ((Sgm (dom fss)) | (dom fss1)) c= dom fss by A7, FINSEQ_1:def 13;
then A12: dom fss2 = rng ((Sgm (dom fss)) | (dom fss1)) by A3, RELAT_1:62;
A13: dom fss1 c= dom fs1 by RELAT_1:11;

now :: thesis:

take Z = (Sgm (dom fss)) | (dom fss1); :: thesis:
A14: dom Z = dom fss1 by A8, RELAT_1:11, RELAT_1:62;

hereby :: thesis:

let x be object ; :: thesis:
assume A15: x in d1 ; :: thesis:
reconsider y = Z . x as object ;
take y = y; :: thesis:
thus y in d2 by A12, A14, A15, FUNCT_1:def 3; :: thesis:
thus [x,y] in Z by A14, A15, FUNCT_1:1; :: thesis:

end;

hereby :: thesis:

let y be object ; :: thesis:
assume y in d2 ; :: thesis:
then consider x being object such that
A16: x in dom Z and
A17: y = Z . x by A12, FUNCT_1:def 3;
reconsider x = x as object ;
take x = x; :: thesis:
thus ( x in d1 & [x,y] in Z ) by A13, A8, A16, A17, FUNCT_1:1, RELAT_1:62; :: thesis:

end;

let x, y, z, u be object ; :: thesis:
assume that
A18: [x,y] in Z and
A19: [z,u] in Z ; :: thesis:
A20: z in dom Z by A19, FUNCT_1:1;
A21: u = Z . z by A19, FUNCT_1:1;
A22: u = (Sgm (dom fss)) . z by A20, A21, FUNCT_1:47;
A23: y = Z . x by A18, FUNCT_1:1;
hence ( x = z implies y = u ) by A19, FUNCT_1:1; :: thesis:
A24: x in dom Z by A18, FUNCT_1:1;
then A25: y = (Sgm (dom fss)) . x by A23, FUNCT_1:47;
assume A26: y = u ; :: thesis:
assume A27: x <> z ; :: thesis:
reconsider x = x, z = z as Element of NAT by A24, A20;
A28: x <= len (Sgm (dom fss)) by A11, A24, FINSEQ_3:25;
A29: z <= len (Sgm (dom fss)) by A11, A20, FINSEQ_3:25;
A30: 1 <= z by A11, A20, FINSEQ_3:25;
A31: 1 <= x by A11, A24, FINSEQ_3:25;

per cases by A27, XXREAL_0:1;

suppose x < z ; :: thesis:

hence contradiction by A7, A25, A22, A26, A31, A29, FINSEQ_1:def 13; :: thesis:

end;

suppose z < x ; :: thesis:

hence contradiction by A7, A25, A22, A26, A28, A30, FINSEQ_1:def 13; :: thesis:

end;

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 A4, FINSEQ_3:40, RELAT_1:11;
A33: rng (Sgm (dom fss1)) = dom fss1 by A13, A5, FINSEQ_1:def 13;

now :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom fs2 ; :: thesis:
then A34: x in dom (Sgm (dom fss2)) by A2, A6, A32, FUNCT_1:11;
then (Sgm (dom fss2)) . x in dom fss2 by A9, FUNCT_1:def 3;
hence x in dom (Seq fss2) by A34, FUNCT_1:11; :: thesis:

end;

assume x in dom (Seq fss2) ; :: thesis:
then A35: x in dom (Sgm (dom fss1)) by A6, A32, FUNCT_1:11;
then (Sgm (dom fss1)) . x in dom fss1 by A33, FUNCT_1:def 3;
hence x in dom fs2 by A2, A35, FUNCT_1:11; :: thesis:

end;

hence A36: dom fs2 = dom (Seq fss2) by TARSKI:2; :: thesis:
thus dom fs2 = dom fs2 ; :: thesis:
let k be Nat; :: thesis:
assume A37: k in dom fs2 ; :: thesis:
then A38: (Sgm (dom fss1)) . k in dom fss1 by A2, FUNCT_1:11;
A39: (Sgm (dom fss2)) . k in dom fss2 by A36, A37, FUNCT_1:11;
A40: (Sgm (dom fss1)) . k in dom fss1 by A2, A37, FUNCT_1:11;
then A41: fss1 . ((Sgm (dom fss1)) . k) = (Seq fss) . ((Sgm (dom fss1)) . k) by A1, GRFUNC_1:2;
A42: (Sgm (dom fss2)) . k = ((Sgm (dom fss)) * (Sgm (dom fss1))) . k by A7, A12, A8, Th3, RELAT_1:11;
k in dom (Sgm (dom fss1)) by A2, A37, FUNCT_1:11;
then k in dom ((Sgm (dom fss)) * (Sgm (dom fss1))) by A13, A8, A38, FUNCT_1:11;
then A43: (Sgm (dom fss2)) . k = (Sgm (dom fss)) . ((Sgm (dom fss1)) . k) by A42, FUNCT_1:12;
A44: fss2 c= fss by A3, RELAT_1:59;
dom fss1 c= dom (Seq fss) by A1, RELAT_1:11;
then A45: (Sgm (dom fss1)) . k in dom (Sgm (dom fss)) by A40, FUNCT_1:11;
thus (Seq fss2) . k = fss2 . ((Sgm (dom fss2)) . k) by A36, A37, FUNCT_1:12
.= fss . ((Sgm (dom fss)) . ((Sgm (dom fss1)) . k)) by A43, A44, A39, GRFUNC_1:2
.= fss1 . ((Sgm (dom fss1)) . k) by A45, A41, FUNCT_1:13
.= fs2 . k by A2, A37, FUNCT_1:12 ; :: thesis:

end;

hence Seq fss2 = fs2 by FINSEQ_1:13; :: thesis: