let D be non empty set ; :: thesis: for F being non empty SubStr of D *+^
for p, q being Element of F holds p [*] q = p ^ q
let F be non empty SubStr of D *+^ ; :: thesis: for p, q being Element of F holds p [*] q = p ^ q
let p, q be Element of F; :: thesis: p [*] q = p ^ q
H₁(F) c= H₁(D *+^ ) by Th25;
then reconsider p9 = p, q9 = q as Element of (D *+^) by TARSKI:def 3;
thus p [*] q = p9 [*] q9 by Th27
.= p ^ q by Def34 ; :: thesis: verum