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 p' = p, q' = q as Element of (D *+^ ) by TARSKI:def 3;
thus p [*] q = p' [*] q' by Th27
.= p ^ q by Def34 ; :: thesis: verum