let b, c be object ; :: thesis: for fin being FinSequence holds 1 < len ((fin ^ <*b*>) ^ <*c*>)
let fin be FinSequence; :: thesis: 1 < len ((fin ^ <*b*>) ^ <*c*>)
len ((fin ^ <*b*>) ^ <*c*>) = (len (fin ^ <*b*>)) + (len <*c*>) by FINSEQ_1:22;
then len ((fin ^ <*b*>) ^ <*c*>) = (len (fin ^ <*b*>)) + 1 by FINSEQ_1:39;
then len ((fin ^ <*b*>) ^ <*c*>) = ((len fin) + (len <*b*>)) + 1 by FINSEQ_1:22;
then len ((fin ^ <*b*>) ^ <*c*>) = ((len fin) + 1) + 1 by FINSEQ_1:39;
then len ((fin ^ <*b*>) ^ <*c*>) = (len fin) + (1 + 1) ;
then 1 + 1 <= len ((fin ^ <*b*>) ^ <*c*>) by NAT_1:11;
hence 1 < len ((fin ^ <*b*>) ^ <*c*>) by NAT_1:13; :: thesis: verum