let seq, seq1, seq9, seq19 be Complex_Sequence; :: thesis: ( seq is non-zero & seq9 is non-zero implies ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) )
assume that
A1: seq is non-zero and
A2: seq9 is non-zero ; :: thesis: ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
thus (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) + (seq19 /" seq9) by A2, Th36
.= ((seq1 (#) seq9) /" (seq (#) seq9)) + ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th36
.= ((seq1 (#) seq9) + (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th9
.= ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) ; :: thesis: (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9)
thus (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) - (seq19 /" seq9) by A2, Th36
.= ((seq1 (#) seq9) /" (seq (#) seq9)) - ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th36
.= ((seq1 (#) seq9) - (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th14
.= ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ; :: thesis: verum