let x1, x2 be stack of X; :: thesis: ( emp x1 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = x1 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) & emp x2 & ex t being the carrier' of X -valued RedSequence of ConstructionRed X st
( t . 1 = s & t . (len t) = x2 & ( for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) implies x1 = x2 )
assume A19: emp x1 ; :: thesis: ( for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x1 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or not emp x2 or for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x2 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or x1 = x2 )
given t1 being the carrier' of X -valued RedSequence of ConstructionRed X such that A20: ( t1 . 1 = s & t1 . (len t1) = x1 ) and
A21: for i being Nat st 1 <= i & i < len t1 holds
( not emp t1 /. i & t1 /. (i + 1) = pop (t1 /. i) ) ; :: thesis: ( not emp x2 or for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x2 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or x1 = x2 )
assume A22: emp x2 ; :: thesis: ( for t being the carrier' of X -valued RedSequence of ConstructionRed X holds
( not t . 1 = s or not t . (len t) = x2 or ex i being Nat st
( 1 <= i & i < len t & not ( not emp t /. i & t /. (i + 1) = pop (t /. i) ) ) ) or x1 = x2 )
given t2 being the carrier' of X -valued RedSequence of ConstructionRed X such that A23: ( t2 . 1 = s & t2 . (len t2) = x2 ) and
A24: for i being Nat st 1 <= i & i < len t2 holds
( not emp t2 /. i & t2 /. (i + 1) = pop (t2 /. i) ) ; :: thesis: x1 = x2
A25: ( len t1 in dom t1 & len t2 in dom t2 & 1 in dom t1 & 1 in dom t2 ) by FINSEQ_5:6;
defpred S1[ Nat] means ( ( $1 in dom t1 implies $1 in dom t2 ) & ( $1 in dom t2 implies $1 in dom t1 ) & ( $1 in dom t1 implies t1 . $1 = t2 . $1 ) );
A26: S1[ 0 ] by FINSEQ_3:24;
A27: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A28: S1[i] ; :: thesis: S1[i + 1]
per cases ( i = 0 or ex j being Nat st i = j + 1 ) by NAT_1:6;
suppose ex j being Nat st i = j + 1 ; :: thesis: S1[i + 1]
then consider j being Nat such that
A29: i = j + 1 ;
A30: i >= 1 by A29, NAT_1:11;
hereby :: thesis: ( i + 1 in dom t2 iff i + 1 in dom t1 )
assume i + 1 in dom t1 ; :: thesis: i + 1 in dom t2
then i + 1 <= len t1 by FINSEQ_3:25;
then i < len t1 by NAT_1:13;
then ( i in dom t1 & not emp t1 /. i ) by A21, A30, FINSEQ_3:25;
then ( len t2 <> i & i <= len t2 ) by A22, A23, A28, FINSEQ_3:25, PARTFUN1:def 6;
then i < len t2 by XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= len t2 ) by NAT_1:11, NAT_1:13;
hence i + 1 in dom t2 by FINSEQ_3:25; :: thesis: verum
end;
hereby :: thesis: ( i + 1 in dom t1 implies t1 . (i + 1) = t2 . (i + 1) )
assume i + 1 in dom t2 ; :: thesis: i + 1 in dom t1
then i + 1 <= len t2 by FINSEQ_3:25;
then i < len t2 by NAT_1:13;
then ( i in dom t2 & not emp t2 /. i ) by A24, A30, FINSEQ_3:25;
then ( len t1 <> i & i <= len t1 ) by A19, A20, A28, FINSEQ_3:25, PARTFUN1:def 6;
then i < len t1 by XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= len t1 ) by NAT_1:11, NAT_1:13;
hence i + 1 in dom t1 by FINSEQ_3:25; :: thesis: verum
end;
assume A32: i + 1 in dom t1 ; :: thesis: t1 . (i + 1) = t2 . (i + 1)
then ( i + 1 <= len t1 & i + 1 <= len t2 ) by A31, FINSEQ_3:25;
then ( i < len t1 & i < len t2 ) by NAT_1:13;
then A33: ( i in dom t1 & t1 /. (i + 1) = pop (t1 /. i) & i in dom t2 & t2 /. (i + 1) = pop (t2 /. i) ) by A21, A24, A30, FINSEQ_3:25;
then ( t1 /. i = t1 . i & t2 /. i = t2 . i & t1 /. (i + 1) = t1 . (i + 1) & t2 /. (i + 1) = t2 . (i + 1) ) by A32, A31, PARTFUN1:def 6;
hence t1 . (i + 1) = t2 . (i + 1) by A28, A33; :: thesis: verum
end;
end;
end;
A34: for i being Nat holds S1[i] from NAT_1:sch 2(A26, A27);
 dom t1 = dom t2
proof
thus dom t1 c= dom t2 by A34; :: according to XBOOLE_0:def 10 :: thesis: dom t2 c= dom t1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom t2 or x in dom t1 )
thus ( not x in dom t2 or x in dom t1 ) by A34; :: thesis: verum
end;
then len t1 = len t2 by FINSEQ_3:29;
hence x1 = x2 by A20, A23, A25, A34; :: thesis: verum