let S be delta-concrete ManySortedSign ; :: thesis: for i being set
for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds
len p1 = len p2
let i be set ; :: thesis: for p1, p2 being FinSequence st ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) holds
len p1 = len p2
let p1, p2 be FinSequence; :: thesis: ( ( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ) implies len p1 = len p2 )
assume A1:
( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) )
; :: thesis: len p1 = len p2
consider f being Function of NAT ,NAT such that
A2:
for s being set st s in the carrier of S holds
ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S )
and
A3:
for o being set st o in the carrier' of S holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S )
by Def9;
per cases
( ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) )
by A1;
suppose A4:
(
[i,p1] in the
carrier of
S &
[i,p2] in the
carrier of
S )
;
:: thesis: len p1 = len p2then consider j1 being
Element of
NAT ,
q1 being
FinSequence such that A5:
(
[i,p1] = [j1,q1] &
len q1 = f . j1 )
and
[:{j1},((f . j1) -tuples_on (underlay S)):] c= the
carrier of
S
by A2;
consider j2 being
Element of
NAT ,
q2 being
FinSequence such that A6:
(
[i,p2] = [j2,q2] &
len q2 = f . j2 )
and
[:{j2},((f . j2) -tuples_on (underlay S)):] c= the
carrier of
S
by A2, A4;
(
i = j1 &
i = j2 &
p1 = q1 &
p2 = q2 )
by A5, A6, ZFMISC_1:33;
hence
len p1 = len p2
by A5, A6;
:: thesis: verum end; suppose A7:
(
[i,p1] in the
carrier' of
S &
[i,p2] in the
carrier' of
S )
;
:: thesis: len p1 = len p2then consider j1 being
Element of
NAT ,
q1 being
FinSequence such that A8:
(
[i,p1] = [j1,q1] &
len q1 = f . j1 )
and
[:{j1},((f . j1) -tuples_on (underlay S)):] c= the
carrier' of
S
by A3;
consider j2 being
Element of
NAT ,
q2 being
FinSequence such that A9:
(
[i,p2] = [j2,q2] &
len q2 = f . j2 )
and
[:{j2},((f . j2) -tuples_on (underlay S)):] c= the
carrier' of
S
by A3, A7;
(
i = j1 &
i = j2 &
p1 = q1 &
p2 = q2 )
by A8, A9, ZFMISC_1:33;
hence
len p1 = len p2
by A8, A9;
:: thesis: verum end;