let i be Nat; :: thesis: for D being non empty set
for z being Element of (i + 1) -tuples_on D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
let D be non empty set ; :: thesis: for z being Element of (i + 1) -tuples_on D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
let z be Element of (i + 1) -tuples_on D; :: thesis: ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
consider t being Element of i -tuples_on D, s being Element of 1 -tuples_on D such that
A1: z = t ^ s by Th126;
ex d being Element of D st s = <*d*> by Th117;
hence ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*> by A1; :: thesis: verum