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 Th23;
then reconsider p9 = p, q9 = q as Element of (D *+^) ;
thus p [*] q = p9 [*] q9 by Th25
.= p ^ q by Def34 ; :: thesis: verum