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 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;

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;

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 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: ex Z being Element of bool [:omega,omega:] 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 ) ) ) )

then
d1,d2 are_equipotent
;( ( 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 A8, RELAT_1:11, RELAT_1:62;

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 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: ( y = u implies not x <> z )

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: not x <> z

assume A27: x <> z ; :: thesis: contradiction

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;

end;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 A8, RELAT_1:11, RELAT_1:62;

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 ) ) ) )

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 A12, A14, A15, FUNCT_1:def 3; :: thesis: [x,y] in Z

thus [x,y] in Z by A14, A15, FUNCT_1:1; :: thesis: verum

end;( 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 A12, A14, A15, FUNCT_1:def 3; :: thesis: [x,y] in Z

thus [x,y] in Z by A14, A15, FUNCT_1:1; :: thesis: verum

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 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 ) ) )( ( 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 A12, FUNCT_1:def 3;

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 A13, A8, A16, A17, FUNCT_1:1, RELAT_1:62; :: thesis: verum

end;( 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 A12, FUNCT_1:def 3;

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 A13, A8, A16, A17, FUNCT_1:1, RELAT_1:62; :: thesis: verum

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 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: ( y = u implies not x <> z )

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: not x <> z

assume A27: x <> z ; :: thesis: contradiction

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
( x < z or z < x )
by A27, XXREAL_0:1;

end;

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: ( dom fs2 = dom (Seq fss2) & dom fs2 = dom fs2 & ( for k being Nat st k in dom fs2 holds

(Seq fss2) . k = fs2 . k ) )

(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 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: verum

end;

hence
Seq fss2 = fs2
by FINSEQ_1:13; :: thesis: verum(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 ) )

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 ( ( 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 ) )

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: verum

end;hereby :: thesis: ( x in dom (Seq fss2) implies x in dom fs2 )

assume
x in dom (Seq fss2)
; :: thesis: x in dom fs2assume
x in dom fs2
; :: thesis: x in dom (Seq fss2)

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: verum

end;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: verum

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: verum

(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 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: verum