let A be QC-alphabet ; for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let p1, p2 be Element of QC-WFF A; for x1, x2, y1, y2 being bound_QC-variable of A st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let x1, x2, y1, y2 be bound_QC-variable of A; ( All (x1,y1,p1) = All (x2,y2,p2) implies ( x1 = x2 & y1 = y2 & p1 = p2 ) )
assume A1:
All (x1,y1,p1) = All (x2,y2,p2)
; ( x1 = x2 & y1 = y2 & p1 = p2 )
thus
x1 = x2
by A1, Th5; ( y1 = y2 & p1 = p2 )
All (y1,p1) = All (y2,p2)
by A1, Th5;
hence
( y1 = y2 & p1 = p2 )
by Th5; verum