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 A13: dom fss2 = rng ((Sgm (dom fss)) | (dom fss1)) by A3, RELAT_1:62;
A14: dom fss1 c= dom fs1 by RELAT_1:11;

now

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

hereby :: thesis:

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

end;

hereby :: thesis:

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

end;

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

per cases by A30, XXREAL_0:1;

suppose x < z ; :: thesis:

hence contradiction by A7, A27, A24, A29, A34, A32, FINSEQ_1:def 13; :: thesis:

end;

suppose z < x ; :: thesis:

hence contradiction by A7, A27, A24, A29, A31, A33, FINSEQ_1:def 13; :: thesis:

end;

end;

end;

then d1,d2 are_equipotent by TARSKI:def 6;
then card d1 = card d2 by CARD_1:5;
then A35: dom (Sgm d2) = Seg (card d1) by A4, FINSEQ_3:40, RELAT_1:11;
A36: rng (Sgm (dom fss1)) = dom fss1 by A14, A5, FINSEQ_1:def 13;

now

now

let x be set ; :: thesis:

hereby :: thesis:

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

end;

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

end;

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

end;

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