let P1, P2 be m -element FinSequence; :: thesis: ( P1 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
P1 . (i + 1) = [:(P1 . i),(X . (i + 1)):] ) & P2 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
P2 . (i + 1) = [:(P2 . i),(X . (i + 1)):] ) implies P1 = P2 )
assume that
A10: ( P1 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
P1 . (i + 1) = [:(P1 . i),(X . (i + 1)):] ) ) and
A11: ( P2 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
P2 . (i + 1) = [:(P2 . i),(X . (i + 1)):] ) ) ; :: thesis: P1 = P2
defpred S₁[ Nat, set , set ] means $3 = [:$2,(X . ($1 + 1)):];
A12: for n being Nat st 1 <= n & n < m holds
for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A13: ( len P1 = m & ( P1 . 1 = X . 1 or m = 0 ) & ( for n being Nat st 1 <= n & n < m holds
S₁[n,P1 . n,P1 . (n + 1)] ) ) by A10, CARD_1:def 7;
A14: ( len P2 = m & ( P2 . 1 = X . 1 or m = 0 ) & ( for n being Nat st 1 <= n & n < m holds
S₁[n,P2 . n,P2 . (n + 1)] ) ) by A11, CARD_1:def 7;
P1 = P2 from RECDEF_1:sch 7(A12, A13, A14);
hence P1 = P2 ; :: thesis: verum