let S, T be non empty RelStr ; :: thesis: for s being Element of S
for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
let s be Element of S; :: thesis: for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
let t be Element of T; :: thesis: (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
thus (uparrow [s,t]) ` = [: the carrier of S, the carrier of T:] \ (uparrow [s,t]) by YELLOW_3:def 2
.= [: the carrier of S, the carrier of T:] \ [:(uparrow s),(uparrow t):] by YELLOW10:40
.= [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] by ZFMISC_1:103 ; :: thesis: verum