let V be RealLinearSpace; :: thesis: for u, u1, v, v1, x, y being VECTOR of V

for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds

( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )

let u, u1, v, v1, x, y be VECTOR of V; :: thesis: for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds

( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )

let p, q, r, s be Element of (CMSpace (V,x,y)); :: thesis: ( u = p & v = q & u1 = r & v1 = s implies ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) )

assume that

A1: u = p and

A2: v = q and

A3: u1 = r and

A4: v1 = s ; :: thesis: ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )

A5: ( p,q _|_ r,s implies u,v,u1,v1 are_COrtm_wrt x,y )

for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds

( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )

let u, u1, v, v1, x, y be VECTOR of V; :: thesis: for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds

( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )

let p, q, r, s be Element of (CMSpace (V,x,y)); :: thesis: ( u = p & v = q & u1 = r & v1 = s implies ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) )

assume that

A1: u = p and

A2: v = q and

A3: u1 = r and

A4: v1 = s ; :: thesis: ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )

A5: ( p,q _|_ r,s implies u,v,u1,v1 are_COrtm_wrt x,y )

proof

( u,v,u1,v1 are_COrtm_wrt x,y implies p,q _|_ r,s )
assume
p,q _|_ r,s
; :: thesis: u,v,u1,v1 are_COrtm_wrt x,y

then [[p,q],[r,s]] in the orthogonality of (CMSpace (V,x,y)) by ANALMETR:def 5;

then consider u19, u29, v19, v29 being VECTOR of V such that

A6: [u,v] = [u19,u29] and

A7: [u1,v1] = [v19,v29] and

A8: u19,u29,v19,v29 are_COrtm_wrt x,y by A1, A2, A3, A4, Def6;

A9: u = u19 by A6, XTUPLE_0:1;

A10: v = u29 by A6, XTUPLE_0:1;

u1 = v19 by A7, XTUPLE_0:1;

hence u,v,u1,v1 are_COrtm_wrt x,y by A7, A8, A9, A10, XTUPLE_0:1; :: thesis: verum

end;then [[p,q],[r,s]] in the orthogonality of (CMSpace (V,x,y)) by ANALMETR:def 5;

then consider u19, u29, v19, v29 being VECTOR of V such that

A6: [u,v] = [u19,u29] and

A7: [u1,v1] = [v19,v29] and

A8: u19,u29,v19,v29 are_COrtm_wrt x,y by A1, A2, A3, A4, Def6;

A9: u = u19 by A6, XTUPLE_0:1;

A10: v = u29 by A6, XTUPLE_0:1;

u1 = v19 by A7, XTUPLE_0:1;

hence u,v,u1,v1 are_COrtm_wrt x,y by A7, A8, A9, A10, XTUPLE_0:1; :: thesis: verum

proof

hence
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
by A5; :: thesis: verum
assume
u,v,u1,v1 are_COrtm_wrt x,y
; :: thesis: p,q _|_ r,s

then [[u,v],[u1,v1]] in the orthogonality of OrtStr(# the carrier of V,(CORTM (V,x,y)) #) by Def6;

hence p,q _|_ r,s by A1, A2, A3, A4, ANALMETR:def 5; :: thesis: verum

end;then [[u,v],[u1,v1]] in the orthogonality of OrtStr(# the carrier of V,(CORTM (V,x,y)) #) by Def6;

hence p,q _|_ r,s by A1, A2, A3, A4, ANALMETR:def 5; :: thesis: verum