let i be natural Number ; :: thesis: for D being non empty set
for z being Tuple of i + 1,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 Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
let z be Tuple of i + 1,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 Th104;
ex d being Element of D st s = <*d*> by Th95;
hence ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*> by A1; :: thesis: verum