let p, q be Element of HP-WFF ; :: thesis: for t being FinSequence st p = q ^ t holds
p = q
let t be FinSequence; :: thesis: ( p = q ^ t implies p = q )
defpred S₁[ Nat] means for p, q being Element of HP-WFF
for t being FinSequence st len p = $1 & p = q ^ t holds
p = q;
A1: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A2: for k being Nat st k < n holds
for p, q being Element of HP-WFF
for t being FinSequence st len p = k & p = q ^ t holds
p = q ; :: thesis: S₁[n]
let p, q be Element of HP-WFF ; :: thesis: for t being FinSequence st len p = n & p = q ^ t holds
p = q
let t be FinSequence; :: thesis: ( len p = n & p = q ^ t implies p = q )
assume that
A3: len p = n and
A4: p = q ^ t ; :: thesis: p = q
len q >= 1 by Th10;
then A5: p . 1 = q . 1 by A4, FINSEQ_1:64;

per cases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;

suppose p is conjunctive ; :: thesis: p = q

then consider r, s being Element of HP-WFF such that
A6: p = r '&' s ;
q . 1 = (<*2*> ^ (r ^ s)) . 1 by A5, A6, FINSEQ_1:32
.= 2 by FINSEQ_1:41 ;
then q is conjunctive by Th12;
then consider r9, s9 being Element of HP-WFF such that
A7: q = r9 '&' s9 ;
<*2*> ^ ((r9 ^ s9) ^ t) = (<*2*> ^ (r9 ^ s9)) ^ t by FINSEQ_1:32
.= (<*2*> ^ r) ^ s by A4, A6, A7, FINSEQ_1:32
.= <*2*> ^ (r ^ s) by FINSEQ_1:32 ;
then (r9 ^ s9) ^ t = r ^ s by Th2;
then A8: r9 ^ (s9 ^ t) = r ^ s by FINSEQ_1:32;

now :: thesis: p = q

per cases ( len r <= len r9 or len r >= len r9 ) ;

suppose A9: len r <= len r9 ; :: thesis: p = q

n = (len q) + (len t) by A3, A4, FINSEQ_1:22;
then len q <= n by NAT_1:11;
then A10: len r9 < n by A7, Th15, XXREAL_0:2;
ex t1 being FinSequence st r ^ t1 = r9 by A8, A9, FINSEQ_1:47;
then r = r9 by A2, A10;
then A11: s9 ^ t = s by A8, FINSEQ_1:33;
len s < n by A3, A6, Th15;
then s9 = s by A2, A11;
then t = {} by A11, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; :: thesis: verum

end;

suppose len r >= len r9 ; :: thesis: p = q

then A12: ex t1 being FinSequence st r9 ^ t1 = r by A8, FINSEQ_1:47;
len r < n by A3, A6, Th15;
then r = r9 by A2, A12;
then A13: s9 ^ t = s by A8, FINSEQ_1:33;
len s < n by A3, A6, Th15;
then s9 = s by A2, A13;
then t = {} by A13, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; :: thesis: verum

end;

end;

end;

hence p = q ; :: thesis: verum

end;

suppose p is conditional ; :: thesis: p = q

then consider r, s being Element of HP-WFF such that
A14: p = r => s ;
q . 1 = (<*1*> ^ (r ^ s)) . 1 by A5, A14, FINSEQ_1:32
.= 1 by FINSEQ_1:41 ;
then q is conditional by Th11;
then consider r9, s9 being Element of HP-WFF such that
A15: q = r9 => s9 ;
<*1*> ^ ((r9 ^ s9) ^ t) = (<*1*> ^ (r9 ^ s9)) ^ t by FINSEQ_1:32
.= (<*1*> ^ r) ^ s by A4, A14, A15, FINSEQ_1:32
.= <*1*> ^ (r ^ s) by FINSEQ_1:32 ;
then (r9 ^ s9) ^ t = r ^ s by Th2;
then A16: r9 ^ (s9 ^ t) = r ^ s by FINSEQ_1:32;

now :: thesis: p = q

per cases ( len r <= len r9 or len r >= len r9 ) ;

suppose A17: len r <= len r9 ; :: thesis: p = q

n = (len q) + (len t) by A3, A4, FINSEQ_1:22;
then len q <= n by NAT_1:11;
then A18: len r9 < n by A15, Th16, XXREAL_0:2;
ex t1 being FinSequence st r ^ t1 = r9 by A16, A17, FINSEQ_1:47;
then r = r9 by A2, A18;
then A19: s9 ^ t = s by A16, FINSEQ_1:33;
len s < n by A3, A14, Th16;
then s9 = s by A2, A19;
then t = {} by A19, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; :: thesis: verum

end;

suppose len r >= len r9 ; :: thesis: p = q

then A20: ex t1 being FinSequence st r9 ^ t1 = r by A16, FINSEQ_1:47;
len r < n by A3, A14, Th16;
then r = r9 by A2, A20;
then A21: s9 ^ t = s by A16, FINSEQ_1:33;
len s < n by A3, A14, Th16;
then s9 = s by A2, A21;
then t = {} by A21, FINSEQ_1:87;
hence p = q by A4, FINSEQ_1:34; :: thesis: verum

end;

end;

end;

hence p = q ; :: thesis: verum

end;

suppose A22: p is simple ; :: thesis: p = q

A23: q <> {} by Th10, CARD_1:27;
ex n being Element of NAT st p = prop n by A22;
hence p = q by A4, A23, FINSEQ_1:88; :: thesis: verum

end;

suppose A24: p = VERUM ; :: thesis: p = q

q <> {} by Th10, CARD_1:27;
hence p = q by A4, A24, FINSEQ_1:88; :: thesis: verum

end;

end;

end;

A25: for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
len p = len p ;
hence ( p = q ^ t implies p = q ) by A25; :: thesis: verum