let K, L be non empty ComplStr ; :: thesis: for x being Element of K
for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `
let x be Element of K; :: thesis: for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `
let y be Element of L; :: thesis: ( the Compl of K = the Compl of L & x = y implies x ` = y ` )
assume ( the Compl of K = the Compl of L & x = y ) ; :: thesis: x ` = y `
then x ` = the Compl of L . y by ROBBINS1:def 3
.= y ` by ROBBINS1:def 3 ;
hence x ` = y ` ; :: thesis: verum